Das λ-Kalkül - die kleinste Programmiersprache

Idee: 1900 stellt Hilbert die Frage nach der Existenz einem automatischen Verfahren, mit dem man alle Sätze der Mathematik beweisen kann.
Turing und Church beweisen 1930, dass es ein solches Verfahren nicht gibt.
Das λ-Kalkül bildet die mathematische Grundlage für funktionale Programmiersprachen.

<name>        := a | b | c | a1 | b2...
<expression>  := <name> | <function> | <application>

<function>    := λ<name>.<expression>
<application> := <expression><expression>

Reduzieren von Ausdrücken:

λx.x y → y
(λx.xy)z → zy
(λx.(λy.xy))ab → (λy.ay)b → ab

Zahlen

0 ≡ λs(λz.z)
1 ≡ λs(λz.s(z))
2 ≡ λs(λz.s(s(z)))
usw.

Funktionen

Nachfolgefunktion:
 S ≡ λwyz.y(wyz)
 5S4 ≡ S(S(S(S(S(4))))) ≡ 9

True:  T ≡ λxy.x
False: F ≡ λxy.y

And: ∧ ≡ λxy.xyF
Or:  &or ≡ λxy.xTy
Not: ¬ ≡ λx.xFT

Links

Das gefürchtete Lambda-Kalkül - Ist leider nicht mehr online! Wer eine Kopie findet, bitte eintragen.
Kurze Wikipedia-Erläuterung zur Lambda-Notation