Lambda-Kalkül
Der Lambda-Kalkül ist eine formale Sprache zur Untersuchung von Funktionen.
| Inhaltsverzeichnis |
Geschichte
Der Lambda-Kalkül wurde von Alonzo Church und Stephen Kleene in den 1930er 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.Allg. 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) = x2 + 2x + 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 Buchstabe L) verwendet
λx.x2 + 2x + 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 Programmiersprache LISP definiert.
Um die oft erwähnte schlichte Eleganz des Lambda-Kalküls zu verdeutlichen, wird hier kurz auf die Grundlagen eingegangen. Man beachte, dass diese Beschreibung schon ein Turing-vollständiges System ist.
In Anlehnung an den Lambda-Kalkül wurde für die Beschreibung nebenläufiger Prozesse der Pi-Kalkül von Robin Milner entwickelt.
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, auch Abstraktion genannt)
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 alle freien Vorkommen von x in T mit S substituiert werden.
Wenn durch β> ein Lambda in ein anderes eingesetzt wird, die sich beide auf dasselbe Atom beziehen, muss 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.Allg. 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.
- bei der sogenannten de-Bruijn-Notation werden die Variablennamen weggelassen. Stattdessen werden Zahlen geschrieben, die die Anzahl der Lambda-Terme zwischen der Variable (also eine Zahl) und dem bindenden Lambda-Ausdruck angibt.
Beispiele
- λx.x ist die Identitätsfunktion. (λx.x a) β> a
- Wenn man wahr als Abkürzung für λx.λy.x versteht und falsch als Abkürzung für λx.λy.y, dann ist der Term λx.λy.((x y) falsch) eine Möglichkeit (von vielen), die logische Funktion und darzustellen, denn er erfüllt die Forderungen, die man an die Funktion und stellt:
- ((und wahr) wahr) = wahr
- ((und wahr) falsch) = falsch
- ((und falsch) wahr) = falsch
- ((und falsch) falsch) = falsch
Siehe auch
Weblinks
- Das gefürchtete Lambda-Kalkül
- Einführung in den λ-Kalkül Gute Einführung in den λ-Kalkül (ca. 100 Seiten, als PS und PDF Dokument)