Mit Hilfe der bereits definierten Ausdrücke, ließe sich die Addition zweier Zahlen recht einfach als rekursive Definition schreiben.
add = (λ xy . (if-then-else (zero? x) y (add (pred x) (succ y))))
Eine solche rekursive Funktion ist im λ-Kalkulus allerdings nicht möglich.
Glücklicherweise gibt es aber eine andere Möglichkeit die Additionsfunktion zu erzeugen. Dafür wird zunächst der rekursive Aufruf aus der Funktionsdefinition entfernt und durch einen Parameter ersetzt.
f = (λ g . (λ xy . (if-then-else (zero? x) y (g (pred x) (succ y)))))
Die gesuchte Additionsfunktion ist ein Fixpunkt dieser Funktion f.
add = (f add)
Alles was nun noch fehlt, ist eine Funktion, die den Fixpunkt einer beliebigen anderen Funktion ermitteln kann. Diese Funktion existiert und wird Υ-Kombinator genannt.
add = (Υ f)
Ein Kombinator (combinator) ist ein λ-Ausdruck, in dem keine freie Variable vorkommt. Ein besonderer Kombinator ist der ω-Kombinator (gr. omega), der sein einziges Argument auf sich selbst anwendet.
ω = (λ x . (x x))
Wendet man diesen Ausdruck auf sich selbst an, so entsteht ein Ω (gr. Omega) genannter Ausdruck.
Ω = ((λ x . (x x)) (λ x . (x x)))
Dieser Ausdruck ist β-redizibel, erzeugt bei der Reduktion aber sich selbst. Er besitzt keine Normalform.
Der Υ-Kombinator entsteht durch hinzufügen eines weiteren Parameters zum Ω-Ausdruck.
Υ = (λ f . ((λ x . (f (x x))) (λ x . (f (x x)))))
Der Υ-Kombinator hat die Eigenschaft, den Fixpunkt eines beliebigen Ausdrucks zu erzeugen.
| (Υ E) | = | ((λ f . ((λ x . (f (x x))) (λ x . (f (x x))))) E) |
| = | ((λ x . (E (x x))) (λ x . (E (x x)))) | |
| = | (E ((λ x . (E (x x))) (λ x . (E (x x))))) | |
| = | (E (Υ E)) |
Genau wie der Ω-Ausdruck, ist auch dieser Ausdruck β-reduzibel, erzeugt bei der Reduktion aber nicht nur sich selbst, sondern auch noch einen Aufruf seines Parameters E.
Mit Hilfe des Υ-Kombinators lässt sich nun die Additionsfunktion definieren.
add = (Υ (λ g . (λ xy . (if-then-else (zero? x) y (g (pred x) (succ y))))))
Mit dieser Definition ist der reine λ-Kalkulus ausreichend erweitert um die Addition natürlicher Zahlen durhführen zu können. Dies soll am Beispiel 1 + 1 einmal gezeigt werden.
| one | = | (succ zero) |
| two | = | (succ (succ zero)) |
| add-step | = | (λ g . (λ xy . (if-then-else (zero? x) y (g (pred x) (succ y))) )) |
| add | = | (Υ add-step) |
Und nun der etwas längliche Beweis 1 + 1 = 2.
| (add one one) | = | ((Υ add-step) one one) |
| = | (add-step (Υ add-step) one one) | |
| = | (if-then-else (zero? one) one ((Υ add-step) (pred one) (succ one))) | |
| = | ((zero? one) one ((Υ add-step) (pred one) (succ one))) | |
| = | (false one ((Υ add-step) (pred one) (succ one))) | |
| = | ((Υ add-step) (pred one) (succ one)) | |
| = | (add-step (Υ add-step) (pred one) (succ one)) | |
| = | (if-then-else (zero? (pred one)) (succ one) ((Υ add-step) (pred (pred one)) (succ (succ one)))) | |
| = | ((zero? (pred one)) (succ one) ((Υ add-step) (pred (pred one)) (succ (succ one)))) | |
| = | (true (succ one) ((Υ add-step) (pred (pred one)) (succ (succ one)))) | |
| = | (succ one) | |
| = | (succ (succ zero)) | |
| = | two |