Fachkonzept: Der Lambda-Kalkül

Der Lambda-Kalkül

Der Lambda-Kalkül stellt ein formales System dar, das die Grundlagen der funktionalen Programmierung bildet. Das Kalkül wurde in den 1930er-Jahren vom Mathematiker Alonzo Church entworfen und in den nachfolgenden Jahren von verschiedenen Personen kontinuierlich weiterentwickelt. Mithilfe des Kalküls lassen sich alle berechenbaren Funktionen ausdrücken, womit es Turingmächtig ist.

Ein für die Informatik einflussreiche Verwendung des Kalküls war die Entwicklung der funktionalen Programmiersprache Lisp. Der Informatiker John McCarthy entwickelte diese in den späten 1950er-Jahren und nahm sich dabei das Lambda-Kalkül als Grundlage. Aus der Programmiersprache Lisp entstanden wiederum unzählige weitere funktionale Programmiersprachen - unter anderem die Programmiersprache Racket.

Aufbau des Lambda-Kalküls

Der Aufbau aller zulässigen Lambda-Kalkül-Ausdrücke $\langle \mathcal{L_{\lambda}} \rangle$ ist durch die folgende Grammatik definiert: $$ \begin{align*} \langle \mathcal{L_{\lambda}} \rangle \rightarrow \ &\langle V \rangle \\ |\ &(\lambda\langle V \rangle.\langle \mathcal{L_{\lambda}} \rangle) \\ |\ &(\langle \mathcal{L_{\lambda}} \rangle\ \langle \mathcal{L_{\lambda}} \rangle ) \end{align*} $$ Diese ist wie folgt zu verstehen: Ein korrekter Lambda-Kalkül-Ausdruck $\mathcal{L_{\lambda}}$ ist entweder:

• Eine Variable:
  • Eine Variable dient im Lambda-Kalkül als ein ersetzbarer Platzhalter für einen Ausdruck.
  • $\langle V \rangle$ beschreibt die Menge aller zulässigen Variablen
  • Beispiele: $x$, $y$, $z$ $\in \langle V \rangle$
    
    
• Abstraktionen (Funktionen):
  • Eine Abstraktion hat immer die Form: $(\lambda\langle V \rangle.\langle \mathcal{L_{\lambda}} \rangle)$
  • Beispiele: $\ (\lambda y.y )$,$\ \ \ $$(\lambda x.\lambda y.(y\ x))$
    
    
• Applikationen (Funktionsanwendungen):
  • Eine Applikation hat immer die Form: $(\langle \mathcal{L_{\lambda}} \rangle\ \langle \mathcal{L_{\lambda}} \rangle)$
    Der links stehende Lambda-Kalkül-Ausdruck wird dabei auf den rechts stehenden angewandt.
  • Beispiele: $\ ((\lambda y.y )\ x)$, $\ \ \ $ $((\lambda xy.(x y))\ (\lambda z.z))$

Arithmetik im Lambda-Kalkül

Gemäß der oben definierten Grammatik kennt das Lambda-Kalkül weder mathematische Operatoren noch Zahlen. Diese lassen sich jedoch durch die Bausteine des Lambda-Kalküls codieren.

Die natürlichen Zahlen werden durch Church-Numerale abgebildet. Eine Zahl $n$ wird dabei durch eine Abstraktion codiert, die eine Funktion $f$ erhält und diese $n$-mal auf eine Variable $x$ anwendet. So ergibt sich:

• $ 0 = \lambda fx. x$
• $1 = \lambda fx.(f\ x)$
• $2 = \lambda fx. (f (f\ x))$
• ...
• $n = \lambda fx. (f^{(n)}\ x)$

Ebenso werden mathematische Operatoren als Funktionen definiert, die bei Anwendung auf Church-Numerale das entsprechende Ergebnis als Church-Numeral ergeben. So entspricht die Codierung der mathematischen Addition beispielsweise: $$\lambda m n f x.((m\ f)\ ((n\ f)\ x))$$

(Auf analoge Weise lassen sich auch logische Komponenten wie $true$, $false$, $if$, $and$, $or$ etc. codieren.)

Um die Übersichtlichkeit bei der Arbeit mit dem Lambda-Kalkül zu erhöhen, werden allerdings häufig auch Schreibweisen mit den gängigen Zahlen und Operatoren genutzt.

Eine gängige Schreibweise wie: $$((\lambda yz.y+z)\ 2)\ 3$$ entspricht somit genau genommen dem Lambda-Kalkül-Ausdruck: $$ (( \lambda y z. (((\lambda m n f x.((m\ f)\ ((n\ f)\ x)))\ y)\ z)) \ (\lambda f.\lambda x. f (f x))) \ (\lambda f.\lambda x. f (f (f x))) $$

Schreibkonventionen im Lambda-Kalkül

Zur weiteren Verbesserung der Übersichtlichkeit von Lambda-Kalkül-Ausdrücken gibt es im Lambda-Kalkül einige Schreibkonventionen. Zwei der wichtigsten sind die folgenden:

1. Die äußersten Klammern dürfen weggelassen werden.
   • Beispiel: $\ $ $\lambda y.y+1$ $\ $ entspricht $\ $ $(\lambda y.y+1)$
   • Beispiel: $\ $ $(\lambda y.y+1)\ 17$ $\ $ entspricht $\ $ $((\lambda y.y+1)\ 17)$
     
     
2. Zwei aufeinanderfolgende Abstraktionen dürfen zu einer Abstraktion mit mehreren Parametern zusammengefasst werden.
   • Beispiel: $\ $ $\lambda xy.x+y$ $\ $ entspricht $\ $ $\lambda x.\lambda y.x+y$

Die Beta-Reduktion

Zur Auswertung einer Applikation wird im Lambda-Kalkül schrittweise die Beta-Reduktion angewandt. Dabei wird der Parameter der Abstraktion durch den Lambda-Ausdruck ersetzt, auf den diese angewandt wurde.

Für eine Abstraktion $\lambda v.\mathcal{L}$ mit dem Parameter $v$ und einem Lambda-Ausdruck $\mathcal{L}$ als Funktionskörper ergibt sich bei Applikation der Abstraktion auf den Ausdruck $\mathcal{A}$, dass alle Vorkommen von $v$ in $\mathcal{L}$ durch den Ausdruck $\mathcal{A}$ ersetzt werden. Ein solcher Beta-Reduktionsschritt wird mit $\rightarrow_{\beta}$ angegeben.

• Beispiel: $\ $ $(\lambda x.x)\ 4 \ \ \rightarrow_{\beta}\ \ 4$
• Beispiel: $\ $ $(\lambda x.x)\ (\lambda z.z*z) \ \ \rightarrow_{\beta}\ \ (\lambda z.z*z)$
• Beispiel: $\ $ $((\lambda ab.a+b)\ 17) \ 3 \ \ \rightarrow_{\beta}\ \ (\lambda b.17+b) \ 3 \ \ \rightarrow_{\beta}\ \ 17+3$
• Beispiel: $\ $ $((\lambda xy.(y\ x))\ 6)\ (\lambda a.a*a) \ \ \rightarrow_{\beta}\ \ (\lambda y.(y\ 6))\ (\lambda a.a*a) \ \ \rightarrow_{\beta}\ \ (\lambda a.a*a)\ 6 \ \ \rightarrow_{\beta}\ \ 6*6$