Der λ-Kalkulus wurde ebenfalls in den 1930er Jahren von Alonzo Church und Stephen Cole Kleene entwickelt. Er wurde entwickelt als formales System zur Untersuchung von Funktionsdefinition, Funktionsanwendung und Rekursion.
Im Gegensatz zur Turing Maschine arbeitet der λ-Kalkulus auf einer sehr viel höheren Abstraktionsebene. Während bei der Turing Maschine Struktur und Basisinstruktionen eines sehr einfachen Computers modelliert werden (vergleichbar mit Assembler), modelliert der λ-Kalkulus Funktionen, Funktionsaufrufe und Werte (vergleichbar mit Hochsprachen).
Dadurch eignet sich der λ-Kalkulus hervorragend zur Beschreibung berechenbarer Funktionen.
Der λ-Kalkulus besteht aus gerade einmal drei syntaktischen Elementen:
Variablen im λ-Kalkulus verhalten sich nicht wie Variablen in den meisten Programmiersprachen. Sie definieren keinen veränderbaren Speicherplatz für verschiedene Werte. Sie sind vielmehr Variablen im mathematischen Sinne: Platzhalter für konkrete Werte, wie beispielsweise Funktionsparameter oder Konstanten.
Die genaue Syntax von Variablen ist für den λ-Kalkulus nicht weiter von Bedeutung. In diesem Dokument dürfen Variablenbezeichner aus Buchstaben und einzelnen Sonderzeichen (Bindestrich und Fragezeichen) bestehen.
Desweiteren werden folgende Konventionen für dieses Dokument verwendet:
Im λ-Kalkulus können Funktionen mit einem einzelnen Parameter definiert werden. Dies wird auch Abstraktion genannt.
(λ x . E)
Eine Abstraktion wird eingeleitet durch eine öffnende Klammer gefolgt von dem griechischen kleinen Lambda. Danach folgen der Name des formalen Parameters (in diesem Beispiel x) und der Funktionsrumpf (E), getrennt durch einen Punkt. Abgeschlossen wird die Abstraktion durch die entsprechende schließende Klammer.
Eine Funktion auf ein konkretes Argument anzuwenden wird Applikation genannt. Dafür wird die folgende Syntax verwendet:
(F E)
Die Applikation ist syntaktisch die Folge zweier Ausdrücke, eingefasst in Klammern. Der erste Ausdruck ist die anzuwendende Funktion (F), der zweite Ausdruck das konkrete Funktionsargument (E).
exp ::= var /* variablen */
| ( lambda var . exp ) /* abstaktion */
| ( exp exp ) /* applikation */
;
Die genaue Syntaxregel für Variablen wurde wiederum weggelassen.
Da die Syntax des λ-Kalkulus sehr "klammer-lastig" ist, werden drei Regeln zur Vereinfachung eingeführt.
(((F A) B) C) = (F A B C)
(λ x . (λ y . E)) = (λ xy . E)
(λ x . (E F)) = (λ x . E F)