Lambda Calculus

Jedes Mal, wenn du in JavaScript/Python eine Anonyme Funktion (Lambda) schreibst:

items.map(x => x * 2)

Das x => ... ist Lambda Kalkül pur. Funktionen sind "First Class Citizens". Du kannst sie herumreichen wie Variablen.

1. Alpha-Konversion & Beta-Reduktion

Die Regeln des Spiels.

• Beta-Reduktion: Das "Ausführen". (λx.x+1) 2 wird zu 2+1 wird zu 3. Man ersetzt den Parameter im Körper durch das Argument.
• Alpha-Konversion: Umbenennen. λx.x ist das Gleiche wie λy.y. Namen sind Schall und Rauch.

2. Y-Kombinator

Wie macht man Rekursion ohne Namen? (Eine anonyme Funktion kann sich nicht selbst aufrufen, sie hat ja keinen Namen!). Der magische Y-Kombinator (λf.(λx.f (x x)) (λx.f (x x))) ermöglicht Rekursion in reiner Logik. Danach ist übrigens der berühmte Startup-Accelerator "Y Combinator" benannt.

1. Church-Turing Thesese vs Gödel

Obwohl Church und Turing formal "alles was berechenbar ist" durch den Lambda-Kalkül und die Turing-Maschine bewiesen, existiert eine philosophische Unterscheidung: Gödel’s Unvollständigkeitssatz zerschmetterte Hilberts Traum ("Jede Aussage ist beweisbar"). Der Lambda-Kalkül übersetzt "Gödels Unbeweisbarkeit" in das Halteproblem. (λx. x x) (λx. x x) ist der unendliche Loop ($\Omega$ Combinator). Man kann keine Lambda-Funktion schreiben, die eine andere Lambda-Funktion von außen betrachtet und statisch beweist, ob diese in endlicher Zeit zu einer "Normalform" (einem Ausgabewert) reduziert, oder in ein $\Omega$ kollabiert.

2. De-Bruijn-Indizes (Nameless Representation)

Compiler mögen keine Variablennamen. Beim Parsen von Lambda Ausdrücken stört die Alpha-Äquivalenz. Ist $\lambda x. x$ dasselbe wie $\lambda y. y$? GHC (Glasgow Haskell Compiler) wandelt Programme in De-Bruijn-Indizes um. Statt Namen zu vergeben, zählt man, wie viele Lambda-Binder ($\lambda$) man nach außen "zurückgehen" muss, um die Variable zu finden. Aus $\lambda x. (\lambda y. x (y x))$ wird $\lambda (\lambda (2\ (1\ 2)))$. So wird die strukturelle Gleichheit des Codes trivial byte-weise vergleichbar, was Caching und Common Subexpression Elimination massiv beschleunigt.

3. Church Numerals und Typen

Im reinen Lambda-Kalkül gibt es keine Hardware-Integer (Bits). Man codiert Zahlen als "Wie oft wende ich eine Funktion an?". Die Null ist: $c_0 = \lambda f. \lambda x. x$ (Wende $f$ null mal an). Die Zwei ist: $c_2 = \lambda f. \lambda x. f(f(x))$. Das ist extrem rechenintensiv. Addition wird zu Funktionskomposition geformt: $c_A + c_B = \lambda f. \lambda x. c_A f\ (c_B\ f\ x)$. Pure untypisierte Lambda-Sprachen sind T-Complete, kollabieren aber bei Endlosschleifen. Führt man das Simply Typed Lambda Calculus ein (jedes Lambda hat einen strikten Typ), erreicht man ein System, das beweisbar immer terminiert (kein Halteproblem mehr!), dafür schließt man aber die Turing-Vollständigkeit aus (Kein Y-Combinator mehr typisierbar!).