Der Lambda-Kalkül (λ-Kalkül) ist ein formales System zur Untersuchung von Funktionen. Er wurde in den 1930er-Jahren von Alonzo Church und Stephen Cole Kleene an der Princeton University entwickelt und gilt als mathematisches Fundament der funktionalen Programmierung.
Nur drei Bausteine
Der untypisierte Lambda-Kalkül kommt mit drei syntaktischen Konstruktionen aus:
- Variablen, z. B.
x,y— als Platzhalter für Werte. - Abstraktion:
λx. Ausdruckdefiniert eine Funktion mit Parameterx. - Applikation:
f xwendet die Funktionfaufxan.
Damit lässt sich jede berechenbare Funktion darstellen — der Kalkül ist eine minimale, universelle Programmiersprache.
Freie und gebundene Variablen
In λx. x + y ist x an die Abstraktion gebunden, y dagegen frei. Die Alpha-Konversion benennt gebundene Variablen um (λx. x ≡ λy. y), ohne die Bedeutung zu ändern. Die Beta-Reduktion setzt Argumente ein: (λx. Ausdruck) wert wird zu Ausdruck[x := wert] — genau das passiert bei jedem Funktionsaufruf in einer Programmiersprache.
Currying
Mehrstellige Funktionen werden durch Currying als verschachtelte einstellige Funktionen dargestellt: λx. λy. x + y nimmt erst x, dann y. Diese Technik liegt den Lambda-Ausdrücken moderner Sprachen zugrunde, siehe auch Lambda.
Bedeutung für die Informatik
Church beantwortete mit dem Kalkül 1936 das Entscheidungsproblem negativ. Die Church-Turing-These besagt, dass Lambda-Kalkül und Turingmaschine gleich mächtig sind: Sie berechnen exakt dieselben Funktionen. Der Kalkül inspirierte Sprachen wie Lisp, Haskell und ML und ist bis heute das Werkzeug, mit dem Typen, Auswertungsstrategien und Kompilieren formal analysiert werden.
Verwandte Grundlagen: Rekursion, Algorithmus und Deklarative Programmierung.