Begriff
Lambda Prolog
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.
Das normale Prolog basiert auf Horn-Klauseln (First-Order Logic).
Terme sind dumme Bäume: f(a, b).
Aber was, wenn wir Funktionen als Daten haben wollen? ($\lambda x. x+1$).
Was, wenn wir Logik über Logik machen wollen?
Lambda Prolog ($\lambda$Prolog) erweitert Prolog um den Lambda-Kalkül.
Terme können $\lambda$-Funktionen sein.
Die Unifikation ist "Higher-Order Unification".
Damit kann man sehr elegant Compiler, Beweiser und Logiken implementieren.
Merksatz: Eine Erweiterung der Logikprogrammiersprache Prolog, die Terme des einfach typisierten Lambda-Kalküls, polymorphe Typisierung und Implikation in Zielen unterstützt, um Programmierung höherer Ordnung zu ermöglichen.
Wenn du einen Theorem Prover schreibst.
Du musst Quantoren ($\forall x$) darstellen.
In normalem Prolog: Hölle (Variablennamen-Konflikte, Substitution manuell bauen).
In $\lambda$Prolog: $\forall x P(x)$ wird als pi x \ (P x) dargestellt.
Die Sprache kümmert sich automatisch um Namen und Scopes (Higher-Order Abstract Syntax).
1. Higher-Order Unification
Ist unentscheidbar (Huet). Aber in der Praxis (für "Pattern"-Probleme, die oft auftreten) gibt geschickte Algorithmen (Miller Patterns). $\lambda$Prolog nutzt diese eingeschränkte Unifikation, um performant zu bleiben.
2. Implikation im Goal
Normale Logik: P :- Q. (Um P zu zeigen, zeige Q).
$\lambda$Prolog erlaubt: (A => B) :- ...
"Nimm an, A ist wahr. Zeige dann B."
Das erlaubt temporäre Annahmen (Hypothetical Reasoning) direkt in der Sprache.
1. HOAS (Higher-Order Abstract Syntax)
Der größte Durchbruch von $\lambda$Prolog ist die Unterstützung von HOAS.
In klassischen Compilern muss man Variablen mit Strings ("x", "y") darstellen und sich manuell um "Alpha-Konvertierung" (Umbenennung zur Vermeidung von Namenskollisionen) kümmern.
In HOAS nutzt man die Lambdas der Metasprache ($\lambda$Prolog), um Variablen der Objektsprache (z. B. Mini-Java) darzustellen.
Ein let x = 5 in x + 1 wird intern zu let 5 (x \ plus x 1).
Dadurch "erbt" man das komplette Variablen-Management, Scoping und Substitution vom Lambda-Palkül. Dies reduziert den Code für einen verifizierten Compiler um ca. 70%.
2. Miller Patterns & LNA-Unifikation
Higher-Order Unification ist im allgemeinen Fall unentscheidbar. Aber Dale Miller entdeckte eine Teilmenge: die Miller Patterns (auch $L_\lambda$-Logik). Dabei dürfen Funktionen nur auf unterschiedliche, gebundene Variablen angewendet werden (z.B. $F x y$). Diese Einschränkung ist mächtig genug für fast alle Aufgaben in der Sprachanalyse, bleibt aber entscheidbar und hat einen eindeutigen "Most General Unifier" (MGU). $\lambda$Prolog-Engines wie Teyjus nutzen spezialisierte abstrakte Maschinen, um diese Unifikation so schnell wie klassische Prolog-Unifikation durchzuführen.
3. Abella und formale Semantik
In der Forschung wird $\lambda$Prolog oft als Engine unter Abella genutzt – einem interaktiven Theorembeweiser für die Eigenschaften von Programmiersprachen. Da $\lambda$Prolog nativ versteht, was ein "Scope" ist, kann man damit in wenigen Zeilen beweisen, dass eine Optimierung in einem Compiler (z.B. "Constant Folding") die Semantik des Programms nicht verändert. Während man in Coq hunderte Zeilen Beweis für "Umbenennungen" schreiben müsste, passiert das in der $\lambda$Prolog-Welt "by design".
Quick-Check
Benutzt das wer?
Forscher. Es ist die Basis für Systeme wie Abella oder ELPI. Nicht für Webserver.Warum Lambda?
Der griechische Buchstabe $\lambda$ steht für anonyme Funktionen. Alonzo Church erfand ihn.Prolog gestorben?
Als Sprache: Nische. Als Idee (Unifikation, Suche): Lebt überall (Datalog, Type Systems).