Lambda-Kalkül

Grundidee und Bedeutung

Der Lambda-Kalkül ist eine formale Sprache zur Untersuchung von Funktionen. Er beschreibt, wie Funktionen definiert, auf Argumente angewandt und ihre Parameter gebunden werden. Eingeführt wurde er in den 1930er Jahren von Alonzo Church und Stephen Cole Kleene. Heute bildet er eine wichtige Grundlage der theoretischen Informatik, der Logik höherer Stufe, der Typtheorie, funktionaler Programmiersprachen und der formalen Semantik in der Linguistik.

Der untypisierte Lambda-Kalkül kann präzise ausdrücken, was eine berechenbare Funktion ist. Er ist im Sinne der Berechenbarkeit genauso mächtig wie eine Turingmaschine. Allerdings lässt sich im Allgemeinen nicht algorithmisch entscheiden, ob zwei Lambda-Ausdrücke äquivalent sind. Typisierte Varianten beschränken die erlaubten Ausdrücke und können unter anderem Logik höherer Stufe darstellen.

Die Grundidee lässt sich an der Zuordnung x ↦ x + 2 erklären. Im Lambda-Kalkül schreibt man dafür λx.x + 2. Die λ-Abstraktion λx bindet die Variable x und erzeugt aus dem nachfolgenden Term eine Funktion. In λx.2 kommt x nicht im Funktionsterm vor; der Ausdruck bezeichnet die konstante Funktion, die jedes Argument auf 2 abbildet. Auch Funktionen, deren Ergebnisse oder Argumente wieder Funktionen sind, lassen sich darstellen. So steht λf.λx.f(f(x)) für eine Funktion, die einer Funktion f ihre zweimalige Anwendung zuordnet.

Eine Funktionsanwendung heißt Applikation und wird als f x statt als f(x) geschrieben. Sie ist linksassoziativ: f x y bedeutet (f x) y. Da alle Terme als einstellige Funktionen aufgefasst werden, werden Funktionen mit mehreren Argumenten durch schrittweise Funktionsbildung dargestellt; dieses Prinzip heißt Currying.

Aufbau der Lambda-Terme

In der einfachsten vollständigen Form gibt es genau drei Möglichkeiten, Lambda-Terme zu bilden:

• Jedes Variablensymbol v aus einer mindestens abzählbar-unendlichen Variablenmenge {x, y, z, …} ist ein Term. • Sind t₁ und t₂ Terme, dann ist auch (t₁ t₂) ein Term, nämlich die Applikation von t₁ auf t₂. • Ist v eine Variable und t ein Term, dann ist auch (λv.t) ein Term, nämlich die Abstraktion von t bezüglich v. • Nichts anderes ist ein Term.

In Backus-Naur-Form lautet die Grammatik: Term ::= v | (Term Term) | (λv. Term). Für praktische Anwendungen ergänzt man häufig Konstantensymbole als weitere atomare Terme.

Eine Variable ist frei, wenn sie nicht durch eine passende λ-Abstraktion gebunden wird. Die Menge der freien Variablen FV(t) ist definiert durch FV(v) = {v}, FV(t₁ t₂) = FV(t₁) ∪ FV(t₂) und FV(λv.t) = FV(t) ∖ {v}. Entsprechend gilt für die gebundenen Variablen BV(v) = ∅, BV(t₁ t₂) = BV(t₁) ∪ BV(t₂) und BV(λv.t) = BV(t) ∪ {v}. Ein Lambda-Term ohne freie Variablen heißt Kombinator.

Substitution und Umformungsregeln

Bei einer Substitution s[v ← t] wird jedes freie Vorkommen von v im Term s durch t ersetzt. Gebundene Vorkommen bleiben unverändert. Beispielsweise ergibt ((λx.x) x)[x ← y] den Term ((λx.x) y), weil das x innerhalb von λx.x gebunden, das zweite x dagegen frei ist. Die Substitution ist nur unter Nebenbedingungen definiert: Eine zuvor freie Variable des eingesetzten Terms darf durch die Einsetzung nicht unbeabsichtigt gebunden werden. Falls nötig, müssen gebundene Variablen vorher umbenannt werden.

Die α-Konversion besagt, dass die Namen gebundener Variablen keine inhaltliche Bedeutung haben. Daher beschreiben λx.x und λy.y dieselbe Funktion. Formal gilt (λv.t) ≡ (λw.t[v ← w]), wenn w in t nicht frei vorkommt und an den ersetzten Stellen nicht bereits anders gebunden ist.

Die β-Konversion beschreibt die eigentliche Funktionsanwendung: ((λv.t) t′) ≡ t[v ← t′]. Wird sie nur von links nach rechts ausgeführt, heißt sie β-Reduktion. Dabei werden die freien Vorkommen des Parameters v im Funktionsterm t durch das Argument t′ ersetzt; alle freien Variablen von t′ müssen frei bleiben.

Ein Term befindet sich in β-Normalform, wenn keine β-Reduktion mehr möglich ist. Eine Stelle, an der reduziert werden kann, heißt β-Redex. Ein Term kann mehrere solche Stellen besitzen, sodass unterschiedliche Reduktionsfolgen möglich sind. Nach dem Resultat von Church und Rosser können zwei aus demselben Term abgeleitete Terme stets weiter zu einem gemeinsamen Term abgeleitet werden. Führen mehrere Folgen zu einer Normalform, sind ihre Ergebnisse bis auf α-Konversion gleich. Existiert überhaupt eine Reduktionsfolge zu einer Normalform, erreicht auch die Standard Reduction Order diese, bei der jeweils das im Term erste Lambda verwendet wird.

Nicht jeder Term besitzt eine β-Normalform. Bei (λx.x x)(λx.x x) liefert eine β-Reduktion wieder denselben Term. Für Computerprogramme kann man Variablennamen durch De-Bruijn-Indizes ersetzen. Sie geben die Anzahl der Lambda-Ausdrücke zwischen einer Variable und ihrer bindenden Abstraktion an; dadurch wird die α-Konversion unnötig und die β-Reduktion einfacher.

Optional kommt die η-Konversion hinzu. Sie beschreibt Extensionalität, also den Grundsatz, dass Funktionen gleich sind, wenn sie für alle Argumente dasselbe Ergebnis liefern: λx.f x ≡ f, sofern x keine freie Variable von f ist.

Codierung von Logik und Rekursion

Obwohl Zahlen, Addition und Wahrheitswerte nicht zu den Grundelementen des reinen Lambda-Kalküls gehören, lassen sie sich allein durch Abstraktion und Applikation codieren. Entsprechend können auch Zahlen, Tupel und Listen als Lambda-Ausdrücke dargestellt werden, Zahlen etwa durch Church-Numerale.

Für Wahrheitswerte kann man wahr als λx.λy.x und falsch als λx.λy.y definieren. Beide Ausdrücke wählen eines von zwei Argumenten aus. Eine mögliche Darstellung der logischen Funktion und ist λx.λy.(x y falsch). Durch β-Reduktion erhält man für und wahr wahr das Ergebnis wahr. Die drei übrigen Kombinationen und wahr falsch, und falsch wahr sowie und falsch falsch ergeben jeweils falsch.

Auch rekursive Funktionen lassen sich ausdrücken. Dazu dient beispielsweise der Fixpunkt-Kombinator Y = λg.(λx.g (x x))(λx.g (x x)). Er ist ein Lambda-Term, mit dem beliebige rekursive Funktionen dargestellt werden können.

Typisierter Lambda-Kalkül

Der typisierte Lambda-Kalkül betrachtet nur Ausdrücke, denen sich durch Typinferenzregeln ein Typ zuordnen lässt. Im einfachsten, von Church in seiner Theory of Simple Types vorgestellten System werden Typen durch TT ::= I | O | (TT → TT) gebildet. I steht für Individuen und kann etwa als Typ der Zahlen verstanden werden; O steht für Wahrheitswerte. τ₁ → τ₂ ist der Typ einer Funktion, die Argumente vom Typ τ₁ auf Ergebnisse vom Typ τ₂ abbildet.

Eine Umgebung Γ ordnet Variablensymbolen Typen zu. Ein Typurteil Γ ⊢ E:T bedeutet, dass der Ausdruck E in der Umgebung Γ den Typ T besitzt. Für eine Variable v gilt Γ ⊢ v:Γ(v). Eine Applikation (t₁ t₂) hat den Typ τ₂, wenn t₁ den Funktionstyp τ₁ → τ₂ und t₂ den Argumenttyp τ₁ besitzt. Eine Abstraktion λa.t hat den Typ τ₁ → τ₂, wenn t unter der um a ↦ τ₁ erweiterten Umgebung den Typ τ₂ hat.

Erweiterungen erlauben Konstanten, Typvariablen wie α, β und γ sowie Typkonstruktoren wie Menge und Liste. Menge(α) bezeichnet beispielsweise den Typ einer Menge mit Elementen vom Typ α. Auch der Pfeil ist ein zweistelliger Typkonstruktor: Pfeil α β entspricht α → β. Typkonstruktoren können ebenfalls durch Currying teilweise angewandt werden.

Es ist entscheidbar, ob ein untypisierter Term typisiert werden kann, selbst wenn Γ unbekannt ist; eine Variante mit Typvariablen und Typkonstruktoren ist der Hindley-Milner-Algorithmus. Die typisierbaren Ausdrücke bilden eine echte Teilmenge aller untypisierten Terme: Der Y-Kombinator ist beispielsweise nicht typisierbar. Dafür ist bei typisierten Ausdrücken die Gleichheit zweier Funktionen modulo α- und β-Konversion entscheidbar. Das Matching-Problem für Lambda-Ausdrücke ist bis zur vierten Ordnung entscheidbar, das allgemeine Unifikationsproblem dagegen unentscheidbar; dafür gibt es praktisch brauchbare approximative Algorithmen.

Anwendungen

In der Informatik bildet der Lambda-Kalkül die formale Grundlage vieler funktionaler Programmiersprachen, darunter Scheme und Lisp. Moderne Sprachen übernehmen insbesondere anonyme Funktionen und Regeln zur Funktionsanwendung. Reale Programmiersprachen enthalten jedoch meist zusätzliche Möglichkeiten, etwa Nebeneffekte, die über den reinen Lambda-Kalkül hinausgehen. Typisierte Varianten beeinflussten Programmiersprachen wie ML und Haskell sowie die Entwicklung von Typsystemen und Theorembeweisern für Logiken höherer Stufe.

In der Linguistik untersucht die Semantik die Bedeutung natürlichsprachlicher Ausdrücke. Die formale Semantik verbindet dafür Prädikatenlogik und Mengenlehre mit Grundlagen des Lambda-Kalküls. Durch Lambda-Abstraktion können unter anderem Propositionen als Eigenschaften sowie komplexere Nominalphrasen, Adjektivphrasen und einige Verbalphrasen dargestellt werden. Eine Grundlage dafür ist die modelltheoretische semantische Interpretation der intensionalen Logik Richard Montagues.