Lambda-Kalkül

Ausgehend von einem mathematischen Term, wie beispielsweise ${\displaystyle x+2}$, lässt sich eine Funktion bilden, die ${\displaystyle x}$ auf ${\displaystyle x+2}$ abbildet. Man schreibt auch ${\displaystyle x\mapsto x+2}$. Beim Lambda-Kalkül geht es zunächst darum, solche Funktionsbildungen sprachlich zu formalisieren. Im Lambda-Kalkül würde man statt ${\displaystyle x\mapsto x+2}$ den Term

• ${\displaystyle \lambda x.x+2}$

schreiben. Man sagt, dass die freie Variable ${\displaystyle x}$ durch λ-Abstraktion gebunden wird. Die Variablen-Bindung kommt in der Mathematik auch in anderen Bereichen vor:

• Mengenlehre: ${\displaystyle \{x\mid \Phi (x)\}}$
• Logik: ${\displaystyle \forall x\;\Phi (x)}$ und ${\displaystyle \exists x\;\Phi (x)}$
• Analysis: ${\displaystyle \int _{0}^{1}f(x)\;\mathrm {d} x}$

Die abstrahierte Variable muss nicht notwendigerweise im Term vorkommen, z. B. ${\displaystyle \lambda x.2}$ . Dieser λ-Ausdruck bezeichnet dann die Funktion, die jedes ${\displaystyle x}$ auf ${\displaystyle 2}$ abbildet. Etwas allgemeiner ist ${\displaystyle \lambda x.y}$ die Funktion, die konstant ${\displaystyle y}$ ist. Wird nachträglich noch nach ${\displaystyle y}$ abstrahiert, so erhält man mit ${\displaystyle \lambda y.\lambda x.y}$ eine Formalisierung der Funktion, die jedem Wert ${\displaystyle y}$ die Funktion zuordnet, die konstant ${\displaystyle y}$ ist. Der Ausdruck ${\displaystyle \lambda y.\lambda x.y}$ repräsentiert also eine funktionswertige Funktion. Im Lambda-Kalkül lassen sich aber auch Funktionen ausdrücken, deren Argumente bereits Funktionen sind. Nimmt man bspw. die Funktion, die jeder Funktion ${\displaystyle f}$ eine andere Funktion ${\displaystyle f^{2}}$ zuordnet, die so entsteht, dass ${\displaystyle f}$ zweimal angewandt wird, so wird ${\displaystyle f^{2}}$ durch den λ-Term ${\displaystyle \lambda x.f(f(x))}$ dargestellt und die Zuordnung ${\displaystyle f\mapsto f^{2}}$ durch ${\displaystyle \lambda f.\lambda x.f(f(x))}$.

Da λ-Terme als Funktionen gesehen werden, kann man sie auf ein Argument anwenden. Man spricht von Applikation und schreibt im Lambda-Kalkül eher ${\displaystyle f~x}$ statt ${\displaystyle f(x)}$. Klammern können Terme gruppieren. Die Applikation als Verbindungsprinzip von Termen ist definitionsgemäß linksassoziativ, d. h. ${\displaystyle f~x~y}$ bedeutet ${\displaystyle (f~x)~y}$. In der üblichen mathematischen Notation würde man hier ${\displaystyle (f(x))(y)}$ schreiben. Wendet man nun einen Lambda-Term ${\displaystyle \lambda x.\theta }$ auf ein Argument ${\displaystyle a}$ an, also ${\displaystyle (\lambda x.\theta )~a}$, so berechnet sich das Ergebnis dadurch, dass in dem Term ${\displaystyle \theta }$ jedes Vorkommen der Variablen ${\displaystyle x}$ durch ${\displaystyle a}$ ersetzt wird. Diese Ableitungsregel nennt man β-Konversion.

λ-Terme formulieren eher allgemeine Prinzipien der Mathematik und bezeichnen nicht so sehr Objekte des üblichen mathematischen Universums. Beispielsweise formuliert ${\displaystyle \lambda x.x}$ das Zuordnungsprinzip der identischen Abbildung, doch diese ist immer auf eine gegebene Menge als Definitionsmenge bezogen. Eine universelle Identität als Funktion ist in der mengentheoretischen Formulierung der Mathematik nicht definiert. Der Lambda-Kalkül im strengen Sinne ist daher eher als ein Neuentwurf der Mathematik zu sehen, in dem die Grundobjekte als universelle Funktionen verstanden werden, im Gegensatz zur axiomatischen Mengenlehre, deren Grundobjekte Mengen sind.

Zahlen und Terme wie ${\displaystyle x+2}$ sind zunächst nicht Bestandteil eines reinen Lambda-Kalküls. Ähnlich wie in der Mengenlehre, in der man Zahlen und Arithmetik allein aus dem Mengenbegriff heraus konstruieren kann, ist es aber auch im Lambda-Kalkül möglich, auf der Basis von λ-Abstraktion und Applikation die Arithmetik zu definieren. Da im Lambda-Kalkül jeder Term als einstellige Funktion verstanden wird, muss eine Addition als die Funktion verstanden werden, die jeder Zahl ${\displaystyle y}$ diejenige (einstellige) Funktion zuordnet, die zu jeder Zahl ${\displaystyle x}$ den Wert ${\displaystyle y}$ addiert (s. Currying).

Lambda-Terme ohne freie Variablen werden auch als Kombinatoren bezeichnet. Die Kombinatorische Logik (oder Kombinator-Kalkül) kann als alternativer Ansatz zum Lambda-Kalkül gesehen werden.

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

Term ::= a (Variable) | (Term Term) (Applikation) | λa. Term (Abstraktion)

wobei ${\displaystyle a}$ für ein beliebiges Symbol aus einer mindestens abzählbar-unendlichen Menge von Variablensymbolen (kurz: Variablen) steht. Für praktische Zwecke wird der Lambda-Kalkül üblicherweise noch um eine weitere Sorte von Termen, die Konstantensymbole, erweitert.

Die Menge der freien Variablen ${\displaystyle FV(T)}$ kann induktiv über der Struktur eines λ-Terms ${\displaystyle T}$ wie folgt definiert werden:

1. ${\displaystyle FV(a)=\{a\}}$, falls der Term eine Variable ${\displaystyle a}$ ist
2. ${\displaystyle FV(T_{1}~T_{2})=FV(T_{1})\cup FV(T_{2})}$ für Applikationen, und
3. ${\displaystyle FV(\lambda a.T)=FV(T)\setminus \{a\}}$, falls der Term eine Abstraktion ist, sind seine freien Variablen die freien Variablen von ${\displaystyle T}$ außer ${\displaystyle a}$.

Die Menge der gebundenen Variablen ${\displaystyle B(T)}$ eines Terms ${\displaystyle T}$ errechnet sich auch induktiv:

1. ${\displaystyle B(a)=\emptyset }$, falls der Term eine Variable ${\displaystyle a}$ ist
2. ${\displaystyle B(T_{1}~T_{2})=B(T_{1})\cup B(T_{2})}$ für Applikationen, und
3. ${\displaystyle B(\lambda a.T)=B(T)\cup \{a\}}$, falls der Term eine Abstraktion ist, sind seine gebundenen Variablen die gebundenen Variablen von ${\displaystyle T}$ vereinigt ${\displaystyle a}$.

Mittels der Definition von freien und gebundenen Variablen kann nun der Begriff der (freien) Variablensubstitution (Einsetzung) induktiv definiert werden durch:

1. ${\displaystyle a[x\leftarrow T]=a}$ falls Variable ${\displaystyle x}$ ungleich ${\displaystyle a}$
2. ${\displaystyle a[a\leftarrow T]=T}$
3. ${\displaystyle (T_{1}~T_{2})[x\leftarrow T]=(T_{1}[x\leftarrow T]~T_{2}[x\leftarrow T])}$
4. ${\displaystyle (\lambda a.T')[a\leftarrow T]=(\lambda a.T')}$
5. ${\displaystyle (\lambda a.T')[x\leftarrow T]=(\lambda a.T'[x\leftarrow T])}$ falls Variable ${\displaystyle x}$ ungleich ${\displaystyle a}$ und falls ${\displaystyle FV(T)}$ disjunkt von ${\displaystyle B(\lambda a.T')}$.

Hinweis: ${\displaystyle S[x\leftarrow T]}$ steht für: ${\displaystyle S}$, in dem die freie Variable ${\displaystyle x}$ durch ${\displaystyle T}$ ersetzt wurde (falls ${\displaystyle x}$ nicht in ${\displaystyle S}$ vorhanden ist, wird auch nichts ersetzt).

Man beachte, dass die Substitution nur partiell definiert ist; ggf. müssen gebundene Variablen geeignet umbenannt werden (siehe α-Kongruenz im Folgenden), so dass niemals eine freie Variable in einem Substitut durch Einsetzung für eine Variable gebunden wird.

Über der Menge der λ-Terme können nun Kongruenzregeln (hier ≡ geschrieben) definiert werden, die die Intuition formal fassen, dass zwei Ausdrücke dieselbe Funktion beschreiben. Diese Relationen sind durch die sogenannte α-Konversion, die β-Konversion sowie die η-Konversion erfasst.

Die α-Konversionsregel formalisiert die Idee, dass die Namen von gebundenen Variablen „Schall und Rauch“ sind; z. B. beschreiben ${\displaystyle \lambda x.x}$ und ${\displaystyle \lambda y.y}$ dieselbe Funktion. Allerdings sind die Details nicht ganz so einfach wie es zunächst erscheint: Eine Reihe von Einschränkungen müssen beachtet werden, wenn gebundene Variablen durch andere gebundene Variablen ersetzt werden.

Formal lautet die Regel wie folgt:

${\displaystyle \lambda V.E~\equiv ~\lambda W.E[V\leftarrow W]}$

falls ${\displaystyle W}$ in ${\displaystyle E}$ nirgends frei vorkommt und ${\displaystyle W}$ in ${\displaystyle E}$ dort nicht gebunden ist, wo es ein ${\displaystyle V}$ ersetzt. Da eine Kongruenzregel in jedem Teilterm anwendbar ist, erlaubt sie die Ableitung, dass ${\displaystyle \lambda x.(\lambda x.x)~x}$ gleich ${\displaystyle \lambda y.(\lambda x.x)~y}$ ist.

Die β-Konversionsregel formalisiert das Konzept der „Funktionsanwendung“. Wird sie ausschließlich von links nach rechts angewandt, spricht man auch von β-Reduktion. Formal lässt sie sich durch

${\displaystyle ((\lambda V.E)~E')~\equiv ~E[V\leftarrow E']}$

beschreiben, wobei alle freien Variablen in ${\displaystyle E'}$ in ${\displaystyle E[V\leftarrow E']}$ frei bleiben müssen (siehe Nebenbedingung bei der Substitutionsdefinition).

Ein Term heißt in β-Normalform, wenn keine β-Reduktion mehr anwendbar ist (nicht für alle Terme existiert eine β-Normalform; siehe unten). Ein tiefes Resultat von Church und Rosser über den λ-Kalkül besagt, dass die Reihenfolgen von α-Konversionen und β-Reduktionen in gewissem Sinn keine Rolle spielt: wenn man einen Term zu zwei Termen ${\displaystyle T_{1}}$ und ${\displaystyle T_{2}}$ ableitet, gibt es immer eine Möglichkeit, ${\displaystyle T_{1}}$ und ${\displaystyle T_{2}}$ jeweils zu einem gemeinsamen Term ${\displaystyle T_{3}}$ abzuleiten.

Die η-Konversion kann optional zum Kalkül hinzugefügt werden. Sie formalisiert das Konzept der Extensionalität, d. h., dass zwei Funktionen genau dann gleich sind, wenn sie für alle Argumente dasselbe Resultat liefern. Formal ist die η-Konversion beschrieben durch:

${\displaystyle \lambda x.f~x~\equiv ~f}$, wenn ${\displaystyle x}$ nicht freie Variable von ${\displaystyle f}$ ist.

• Nicht für alle Terme existiert eine β-Normalform. Beispielsweise kann man auf den Term ${\displaystyle (\lambda x.x~x)(\lambda x.x~x)}$ zwar β-Reduktion anwenden, doch man erhält wieder den gleichen Term als Ergebnis zurück.
• Jeder Term, der die Bedingung der β-Regel erfüllt, wird β-reduzibel genannt.
• Die β-Reduktion ist im Allgemeinen nicht eindeutig; es kann mehrere Ansatzpunkte (sog. β-Redexe, von englisch reducible expression, reduzibler Ausdruck) für die Anwendung der β-Regel geben, weil die Regelanwendung in allen Teiltermen möglich ist.
• Wenn mehrere Folgen von β-Reduktionen möglich sind und mehrere davon zu einem nicht-β-reduziblen Term führen, so sind diese Terme bis auf α-Kongruenz 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.
• In einer alternativen Notation werden die Variablennamen durch De-Bruijn-Indizes ersetzt. Diese Indizes entsprechen der Anzahl der Lambda-Terme zwischen der Variablen und ihrem bindenden Lambda-Ausdruck. Diese Darstellung wird oft in Computerprogrammen verwendet, da sie die α-Konversion obsolet macht und β-Reduktion deutlich vereinfacht.

• Der Term ${\displaystyle \lambda x.\lambda y.(x~y~\operatorname {falsch} )}$ ist eine Möglichkeit von vielen, die logische Funktion ${\displaystyle \operatorname {und} }$ darzustellen. Hierzu versteht man ${\displaystyle \operatorname {wahr} }$ als Abkürzung für ${\displaystyle \lambda x.\lambda y.x}$ und ${\displaystyle \operatorname {falsch} }$ als Abkürzung für ${\displaystyle \lambda x.\lambda y.y}$. Der Term erfüllt alle Forderungen, die man an die Funktion ${\displaystyle \operatorname {und} }$ stellt.
  • ${\displaystyle \operatorname {und} ~\operatorname {wahr} ~\operatorname {wahr} ~{\overset {\mathrm {def} }{\equiv }}~(\lambda x.\lambda y.(x~y~\operatorname {falsch} ))~\operatorname {wahr} ~\operatorname {wahr} ~{\overset {\beta \beta }{\equiv }}~\operatorname {wahr} ~\operatorname {wahr} ~\operatorname {falsch} ~{\overset {\mathrm {def} }{\equiv }}~(\lambda x.\lambda y.x)~\operatorname {wahr} ~\operatorname {falsch} ~{\overset {\beta }{\equiv }}~(\lambda y.\operatorname {wahr} )~\operatorname {falsch} ~{\overset {\beta }{\equiv }}~\operatorname {wahr} }$
  • ${\displaystyle \operatorname {und} ~\operatorname {wahr} ~\operatorname {falsch} ~\equiv ~\ldots ~\equiv ~\operatorname {wahr} ~\operatorname {falsch} ~\operatorname {falsch} ~\equiv ~\ldots ~\equiv ~(\lambda y.\operatorname {falsch} )~\operatorname {falsch} ~\equiv ~\operatorname {falsch} }$
  • ${\displaystyle \operatorname {und} ~\operatorname {falsch} ~\operatorname {wahr} ~\equiv ~\operatorname {falsch} ~\operatorname {wahr} ~\operatorname {falsch} ~\equiv ~(\lambda x.\lambda y.y)~\operatorname {wahr} ~\operatorname {falsch} ~\equiv ~(\lambda y.y)~\operatorname {falsch} ~\equiv ~\operatorname {falsch} }$
  • ${\displaystyle \operatorname {und} ~\operatorname {falsch} ~\operatorname {falsch} ~\equiv ~\operatorname {falsch} ~\operatorname {falsch} ~\operatorname {falsch} ~\equiv ~\ldots ~\equiv ~(\lambda y.y)~\operatorname {falsch} ~\equiv ~\operatorname {falsch} }$
• Man kann in ähnlicher Weise Zahlen, Tupel und Listen in λ-Ausdrücken codieren (z. B. durch sogenannte Church-Numerale)
• Man kann beliebige rekursive Funktionen durch den Fixpunkt-Kombinator ${\displaystyle \mathbf {Y} =\lambda g.(\lambda x.g~(x~x))(\lambda x.g~(x~x))}$ darstellen.