Da der reine λ-Kalkulus keine Konstanten oder Funktionen vordefiniert, ist die Algorithmenbeschreibung zunächst sehr umständlich. Er lässt sich aber problemlos um die gängigen Strukturen zur Formulierung von Algorithmen erweitern.
In diesem Kapitel sollen einige dieser Definitionen eingeführt werden. Das Ziel ist es, die Addition zweier natürlicher Zahlen nachbilden zu können.
Die benötigten Strukturen, wie sie auch in jeder Programmiersprache zur Verfügung stehen:
Zunächst werden drei Funktionen definiert, die es ermöglichen Fallunterscheidungen zu treffen.
true und false sind die Konstanten der Bool'schen Logik, Wahr und Falsch. if-then-else ist eine Struktur, die es erlaubt anhand einer bool'schen Bedingung einen von zwei Ausdrücken auszuwählen. Dazu müssen die drei Definitionen folgende Beziehungen erfüllen:
| (if-then-else true E F) | = | E |
| (if-then-else false E F) | = | F |
Eine mögliche Definition sieht wie folgt aus:
| true | = | (λ xy . x) |
| false | = | (λ xy . y) |
| if-then-else | = | (λ ctf . (c t f)) |
Der Beweis für die erste geforderte Beziehung sieht so aus:
| (if-then-else true E F) | = | ((λ ctf . (c t f)) true E F) |
| = | (true E F) | |
| = | ((λ xy . x) E F) | |
| = | E |
Der Beweis für false funktioniert entsprechend.
Als Basis für alle komplexeren Datenstrukturen reicht es aus, ein geordnetes Paar aus zwei Werten zu definieren. Diese Definition findet sich in vielen funktionalen Sprachen in Form des cons-pairs mit den zugehörigen Funktionen cons, car und cdr wieder.
Aus dieser einfachen Datenstruktur lassen sich ohne große Schwierigkeiten alle anderen Datenstrukturen, wie z.B. Listen oder Bäume, aufbauen.
In diesem Dokument werden die Namen der drei Funktionen der Verständlichkeit halber nicht von LISP übernommen, sondern pair, first und second genannt.
Diese drei Funktionen müssen folgende Bedingungen erfüllen:
| (first (pair E F)) | = | E |
| (second (pair E F)) | = | F |
Eine Möglichkeit ist die folgende:
| pair | = | (λ fs . (λ w . (w f s)) |
| first | = | (λ p . (p true)) |
| second | = | (λ p . (p false)) |
Hier kommt die Eigenschaft von true und false, von zwei Argumenten jeweils eines auszuwählen, sehr gelegen. Etwas deutlicher wird dies noch, wenn bei der Definition von pair die Funktion if-then-else verwendet wird.
pair = (λ fs . (λ w . (if-then-else w f s)))
Diese zwei Definitionen sind natürlich equivalent, was problemlos durch Einsetzen und Anwenden der β-reduction bewiesen werden kann.
Der Beweis für die geforderten Bedingungen ist wieder relativ einfach durch wiederholtes einsetzen und vereinfachen zu führen:
| (first (pair E F)) | = | ((λ p . (p true)) (pair E F)) |
| = | ((pair E F) true) | |
| = | (((λ fs . (λ w . (w f s))) E F) true) | |
| = | ((λ w . (w E F)) true) | |
| = | (true E F) | |
| = | ((λ xy . x) E F) | |
| = | E |
Nach dem Mathematiker Giuseppe Peano müssen natürliche Zahlen die folgenden Eigenschaften aufweisen (Peano Axiome):
In Übereinstimmung mit diesen Axiomen werden vier Funktionen definiert:
Aus den Peano Axiomen ergeben sich für die Funktionen folgende Eigenschaften:
| (zero? zero) | = | true |
| (zero? (succ E)) | = | false |
| (pred (succ E)) | = | E |
Eine einfache und relativ gut nachvollziehbare Definition dieser Funktionen basiert auf einer Listendarstellung der natürlichen Zahlen.
Eine Zahl n wird durch eine Liste der Länge n+1 repräsentiert. Alle Listenelement mit Ausnahme des letzten sind false. Das letzte Listenelement ist true und dient der Markierung des Listenendes bzw. der 0.
Aufgebaut werden diese Listen mit Hilfe der pair Funktion, indem das Listenelement im ersten und der Rest der Liste im zweiten Teil des Paares gespeichert wird.
Daraus ergeben sich folgende Definitionen:
| zero | = | (pair true true) |
| zero? | = | (λ n . (first n)) |
| succ | = | (λ n . (pair false n)) |
| pred | = | (λ n . (second n)) |
Die Beweise:
| (zero? zero) | = | ((λ n . (first n)) zero) |
| = | (first zero) | |
| = | (first (pair true true)) | |
| = | true |
| (zero? (succ E)) | = | ((λ n . (first n)) (succ E)) |
| = | (first (succ E)) | |
| = | (first (pair false E)) | |
| = | false |
| (pred (succ E)) | = | ((λ n . (second n)) (succ E)) |
| = | (second (succ E)) | |
| = | (second (pair false E)) | |
| = | E |