Begriff
ACL2
Warum wichtig?
Dieser Begriff ist ein Knoten im SengakujiWorks-Wissensnetz. Nutze Level 0 für die erste Einordnung, Level 1 für Praxis, Level 2 für technische Struktur und Level 3 für Grenzen, Fallstricke und Expertenkontext.
Stell dir vor, deine CPU hat einen Mathe-Fehler (wie der berühmte Pentium-Bug). Das kostet Milliarden. ACL2 ist ein Werkzeug, um Hardware-Designs und Algorithmen mathematisch zu beweisen. Es ist der "Industrie-Bagger" unter den Beweisern. Nicht so elegant wie Coq, aber extrem stark automatisiert. AMD nutzt es, um jede einzelne Fließkomma-Operation ihrer Prozessoren zu beweisen. Es basiert auf der Programmiersprache Lisp ("Code ist Daten, Daten sind Code").
Merksatz: Ein Theorembeweiser für eine Variante von Common Lisp, der industriell für die Verifikation von Mikroprozessoren (AMD) und komplexer Software (JVM) eingesetzt wird.
Es ist eine Programmiersprache.
Du schreibst eine Funktion (defun square (x) (* x x)).
Dann schreibst du ein Theorem: (defthm square-is-positive (>= (square x) 0)).
ACL2 ruft seine Engine auf ("The Waterfall").
Es versucht Simplification, Destructor Elimination, Induction...
Meistens sagt es "Q.E.D.".
Wenn nicht, gibt es dir Hinweise ("Checkpoint"), welche Zwischenschritte fehlen.
1. The Waterfall
Die Architektur von ACL2. Ein Beweis fällt Kaskaden (Wasserfälle) herunter. Phase 1: Vereinfache die Formel. -> Hat es geklappt? Fertig. Nein? -> Phase 2: Zerlege Destruktoren. Nein? -> Phase 3: Nutze gespeicherte Lemmata. Nein? -> Phase 4: Induktion (Der Joker). ACL2 ist extrem gut darin, Induktions-Strategien automatisch zu finden ("Induct on (length x)").
2. Boyer-Moore Logic
Die Logik dahinter. Eine quantorenfreie Logik erster Ordnung mit Rekursion. Sehr nah an der "echten" Programmierung.
1. Symbolic Simulation & GL-Clause-Processor
Eines der mächtigsten Features in der Industrie ist GL. Anstatt jedes Theorem manuell durch Induktion zu führen, erlaubt GL eine symbolische Simulation. Du nimmst deinen Hardware-Code (z. B. ein 64-Bit Addierer) und lässt ACL2 ihn mit symbolischen Variablen durchrechnen. ACL2 wandelt das Problem in eine riesige boolesche Formel um und schickt sie an einen SAT-Solver. Wenn der SAT-Solver sagt "UNSAT" (unerfüllbar), bedeutet das: Es gibt keine Kombination von 0en und 1en, die einen Fehler verursacht. So werden bei AMD ganze ALUs (Arithmetic Logic Units) vollautomatisch verifiziert.
2. Applicative Common Lisp (Die "Pure" Regel)
Das "A" in ACL2 steht für "Applicative".
Das bedeutet: ACL2 unterstützt nur den rein funktionalen Teil von Lisp.
Keine Seiteneffekte, keine globalen Variablen, keine destruktiven Änderungen (setq ist verboten).
Warum? Weil man nur über pure Funktionen mathematisch beweisen kann. f(x) muss immer den gleichen Wert liefern.
Damit ACL2 trotzdem effizient ist, nutzt es im Hintergrund Stobjs (Single-threaded Objects). Diese erlauben es, Daten im Speicher destruktiv zu verändern (für Speed), während die Logik-Engine so tut, als wäre alles rein funktional. Das ist ein genialer Hack, um "Beweisbarkeit" mit "Performance" zu verheiraten.
3. The Book System
ACL2 ist als kleiner Kern konzipiert, der durch Books erweitert wird.
Ein "Book" ist eine Sammlung von bewiesenen Theoremen.
Wenn du ein Dateisystem beweisen willst, lädst du das std/io Book. Willst du Fließkommazahlen prüfen, lädst du das rtl/rel8 Book.
Diese Modularität erlaubt es Teams weltweit, auf den Beweisen anderer aufzubauen. Ein SRE oder Hardware-Architekt bei AMD schreibt nicht alles neu; er nutzt zehntausende von "Rewrite-Rules" aus existierenden Books, die ACL2 sagen: "Wenn du diesen komplexen Ausdruck siehst, vereinfache ihn zu jenem Ausdruck."
Quick-Check
Wer nutzt das?
AMD, Intel, Centaur. Es ist der Standard für Chip-Design-Verifikation.Unterschied zu Coq?
ACL2 ist "First-Order Logic" und automatisiert. Coq ist "Higher-Order Logic" und interaktiv. ACL2 ist "hemdsärmeliger" und pragmatischer für Ingenieure.Warum Lisp?
Weil Lisp die Sprache der symbolischen KI war (in den 70ern/80ern, als Boyer-Moore entstand). Und weil Code-Analyse in Lisp (S-Expressions) trivial ist.