Im λ-Kalkulus spricht man von gebundenden und freien Variable, je nachdem ob eine auftretende Variable dem Parameter eine Abstraktion entspricht. Man sagt, die Abstraktion bindet den Parameter innerhalb des Abstraktionsrumpfes. In dem Ausdruck
(λ x . (x y))
ist die Variable x durch die Abstraktion gebunden. Die Variable y hingegen ist frei. Freie Variablen können durch äussere Abstraktionen gebunden sein.
(λ y . (λ x . (x y)))
Die Variable x ist durch die innere Abstraktion gebunden, die Variable y durch die äussere Abstraktion.
Im λ-Kalkulus gibt es drei Operationen die eine Equivalenzbeziehung zwischen zwei Ausdrücken herstellen.
Die α-conversion (Alpha-Umwandlung) drückt die Idee aus, dass der Name des Parameters für eine Funktion nicht von Bedeutung ist. Wir können den Parameter beliebig umbenennen, solange dadurch keine Namenskonflikte auftreten.
(λ x . E) = (λ y . E[x/y])
Dabei steht E[x/y] für den Ausdruck E mit allen freien Vorkommen von x ersetzt durch y.
Diese Umwandlung ist nur dann gültig, wenn die Variable y in E nicht frei vorkommt, da diese dann nicht mehr von dem Funktionsparameter zu unterscheiden wäre. Aus dem gleichen Grund darf die Umwandlung auch nicht durchgeführt werden, wenn x an einer Stelle auftritt, an der y bereits durch eine Abstraktion gebunden ist.
Die β-reduction (Beta-Reduktion) beschreibt den Gedanken der Funktionsanwendung.
((λ x . E) F) = E[x/F]
Diese Reduktion kann wiederum nur dann ausgeführt werden, wenn alle freien Variablen in F dabei frei bleiben. Unter Umständen muss also vorher eine α-conversion durchgeführt werden.
Die η-conversion (Eta-Umwandlung) gibt die Idee wieder, dass zwei Funktionen equivalent sind, wenn sie für gleiche Argumente stets das gleiche Ergebnis liefern.
(λ x . (E x)) = E
Diese Umwandlung ist natürlich nur dann legal, wenn x in E nicht frei vorkommt.
Einen Ausdruck der keine β-reduction mehr zulässt, also keinen Ausdruck der Form
((λ x . E) F)
enthält, nennt man Normalform.
Wenn ein Ausdruck eine Normalform besitzt, erreicht man diese immer durch Anwendung der β-reduction von links nach rechts (normal order evaluation). Diese Normalform ist, bis auf die Bezeichnung der Parameter, eindeutig und wird auch Wert des Ausdrucks genannt.
Zwei Ausdrücke sind genau dann equivalent, wenn sie die gleiche Normalform besitzen.
Es gibt Ausdrücke, die keine Normalform haben. Beispielsweise der als Ω bezeichnete Ausdruck
((λ x . (x x)) (λ x . (x x)))
Die Abstraktion des λ-Kalkulus erlaubt zunächst nur die Definition von Funktionen mit exakt einem Parameter. Um Funktionen mit mehr als einem Parameter nachbilden zu können, muss eine solche Funktion zunächst in mehrere Funktionen Höherer Ordnung zerlegt werden. Diesen Vorgang nennt man Currying, benannt nach dem Mathematiker Haskell Brooks Curry.
Eine Funktion von n Parametern f(x1…xn) wird in n Funktionen f1…fn zerlegt, die jeweils einen Parameter verarbeiten und eine weitere Funktion erzeugen, die die restlichen Parameter verarbeitet. Die letzte Funktion liefert dann das Ergebnis.
(((f1 x1) x2) x3) = ((f2 x2) x3) = (f3 x3) = y
Als konkretes Beispiel soll hier einmal die Addition der Zahlen 2 und 3 dienen.
(add 2 3) = ((add 2) 3)
Zunächst wird die Funktion add auf das erste Argument 2 angewendet. Dies erzeugt eine neue Funktion add-2 die zu ihrem Parameter jeweils 2 hinzuaddiert. Wendet man diese Funktion nun auf den zweiten Parameter 3, erhält man das korrekte Ergebnis 5.
((add 2) 3) = (add-2 3) = 5