Lambda-Kalkül

Der Lambda-Kalkül ist eine formale Sprache zur Untersuchung von Funktionen. Er wurde von Alonzo Church und Stephen Kleene in den 30er Jahren eingeführt. Church benutzte den Lambda-Kalkül, um 1936 eine negative Antwort auf das Entscheidungsproblem zu geben. Mittels des Kalküls kann man klar definieren, was eine berechenbare Funktion ist. Die Frage, ob zwei Lambda-Ausdrücke (s.u.) äquivalent sind, kann i.a. nicht algorithmisch entschieden werden. Der Lambda-Kalkül hat die Entwicklung funktionaler Programmiersprachen, insbesondere LISPs, wesentlich beeinflusst.

Die übliche Notation einer mathematischen Funktion wie im Beispiel

    f(x) = x*x + 2*x + 10

 

ist in dem Sinne doppeldeutig, dass nicht klar ist, ob man die ganze Funktion mit all ihren Funktionswerten meint oder nur die Funktion an der Stelle x.

Um dies eindeutig anzugeben, wird die so genannte lambda-Notation (griechischer kleiner Buchstaben l) verwendet

  λx [ x*x + 2*x + 10 ]

 

Alonzo Church hat 1941 diese Notation eingeführt.

Gemeinsam mit weiteren Syntax- und Umformungsregeln bildet diese Notation den Lambda-Kalkül: ein vollständiges System zur Beschreibung und Ausführung mathematischer Berechnungen und Verfahren, das im Sinne des Konzepts der Berechenbarkeit ebenso mächtig ist wie beispielsweise die modernen Programmiersprachen oder die Turing-Maschine.

Konrad Zuse hat Ideen aus dem Lambda-Kalkül 1942-1946 in seinen Plankalkül einfließen lassen. John McCarthy hat sie Ende der fünfziger Jahre verwendet und damit die minimalen Funktionen der LISP-Programmiersprache definiert.

Um die oft erwähnte schlichte Eleganz des Lambda-Kalkül zu verdeutlichen, wird hier kurz auf die Grundlagen eingegangen. Man beachte, dass diese Beschreibung schon ein Turing-vollständiges System ist.

Untypisierter Lambda-Kalkül

In seiner einfachsten, dennoch vollständigen, Form gibt es im Lambdakalkül drei Sorten von Termen (T), hier in Backus-Naur-Form:

T := a (Atom)

| (T T) (Applikation)

| λa.T (Lambda)

wobei a für ein beliebiges Symbol aus einer mindestens abzählbar-unendlichen Menge steht, sowie zwei Umformungsregeln:

• α= (Umbenennung) ist die Substitution aller Auftreten eines Atoms in einem Lambda durch ein frisches (bisher unbenutztes) Atom.
• β> (Reduktion) ist die Ersetzung eines Terms der Form (λx.T S) durch T, wobei x mit S substituiert wird.

Wenn durch β> ein Lambda in ein anderes eingesetzt wird, die sich beide auf dasselbe Atom beziehen, muß mit einem von beiden Lambdas vor der Operation α= durchgeführt werden.

Anmerkungen

• Jeder Term, der die Bedingung der β-Regel erfüllt, wird β-Reduzibel genannt.
• β> ist i.A. nicht eindeutig.
• Wenn mehrere Folgen von β-Reduktionen möglich sind, und mehrere davon zu einem nicht-β-reduziblen Term führen, so sind diese Terme bis auf α= gleich.
• Wenn jedoch eine Reihenfolge der β zu einem nicht-β-reduziblen Term (einem Ergebnis) führt, so tut dies auch die Standard Reduction Order, bei der das im Term erste Lambda zuerst verwendet wird.

Beispiele

• λx.x ist die Identitätsfunktion. (λx.x a) β> a
• Wenn λx.λy.x wahr ist und λx.λy.y falsch, dann bildet λx.λy.((x y) wahr) die logische Funktion und.

Siehe auch: Berechenbarkeitstheorie

Weblinks

• Das gefürchtete Lambda-Kalkül