Der Lambda-Kalkül
Aus ProgrammingWiki
Inhaltsverzeichnis |
Einführung
Der λ-Kalkül fasst berechenbare Funktionen zu einer abstrakten Klasse zusammen.
Er wurde um 1936 durch Alonzo Church (* 14. Juni 1903; † 11. August 1995; US-amerikanischer Mathematiker, Logiker und Philosoph; Mitbegründer der theoretischen Informatik) entwickelt und bildet die theoretische Grundlage funktionaler bzw. funktionsorientierter Programmiersprachen.
Hinweis:
Der λ-Kalkül und die Turingmaschine (theoretisches Fundament imperativer Programmiersprachen) beschreiben äquivalente Klassen berechenbarer Funktionen.
Damit sind funktionale bzw. funktionsorientierte Programmiersprachen (z.B. Haskell, Scheme, Logo) und imperative Programmiersprachen (z.B. Visual Basic, Delphi, C++) "gleich mächtig".
Die Grundidee des λ-Kalküls besteht darin, die Klasse der λ-Ausdrücke zu bilden,
- die aus gegebenen Grundbausteinen aufbaut werden und
- für die bestimmte Rechenregeln bestehen.
Definition der λ-Ausdrücke
-
Der Vorrat an Grundbausteinen ist eine (abzählbar) unendliche Menge von Variablen
$\{x_1, x_2, x_3, ...\}$, die selbst λ-Ausdrücke sind.
Beispiele: -
Durch Anwendung des λ-Ausdrucks $M$ auf den λ-Ausdruck $N$ entsteht wieder ein λ-Ausdruck, geschrieben als $(M \; N)$.
Beispiele: -
λ-Ausdrücke können durch funktionale Abstraktion erzeugt werden:
Mit der Variablen $x$ und dem λ-Ausdruck $M$ ist auch
$(\lambda (x) M)$ ein λ-Ausdruck.
Beispiele:
Rechenregeln
β-Reduktion
Sind $E$ und $M$ λ-Ausdrücke, wobei $M$ in $E$ nicht gebunden vorkommen darf, und $x$ eine Variable, so beschreibt
$((\lambda (x) E) M)\stackrel{\beta}{\longrightarrow}E[M/x]$
(sprich: "$E$ mit $M$ für $x$")
das Ergebnis der Anwendung von $(\lambda (x) E)$ auf $M$.
Dabei werden im Ausdruck $E$ alle Variablen $x$ durch den Ausdruck $M$ ersetzt.
Beispiele:
Beachte:
Der λ-Kalkül fordert eine sogenannte leftmost reduction bzw. normal order reduction, d.h. der jeweils links stehende Ausdruck $(\lambda (x) E)$ wird zuerst reduziert.
α-Konvention
Wenn $x'$ in $E$ nicht frei vorkommt, gilt:
$(\lambda (x) E)\stackrel{\alpha}{\longleftrightarrow}(\lambda (x') E[x'/x])$
(sprich: "Ersetze alle $x$ in $(\lambda (x) E)$ durch $x'$")
Beispiele:
η-Umwandlung
Vereinfachungsregel, mit:
$(\lambda (x) (E \; x))\stackrel{\eta}{\longrightarrow}E$
Beispiele:
Aufgaben
-
Implementieren Sie die Prozedur super-ersetzen, die in einer verschachtelten Liste das Element 1 durch das Element 2 ersetzt.
Quelltext überprüfen:
-
Schreiben Sie das Prädikat lambda-term?, das prüft, ob eine vorgegebene Liste ein λ- Ausdruck der Form $(\lambda (x) E)$ ist.
Quelltext überprüfen:
-
Schreiben Sie die Prozedur (lambda-ersetzen <term> <var>), die in einem λ-Term (vgl. Aufgabe 2) alle gebundenen Variablen durch die Variable var ersetzt. Natürlich darf var in diesem λ-Term nicht frei vorkommen.
Beachten Sie dabei, dass λ-Terme selbst beliebige λ-Terme enthalten können (Repräsentation als verschachtelte Listen).
Implementieren Sie die nächste Aufgabe unter DrScheme. Denken Sie an die Definition geeigneter Hilfsprozeduren.
Zum Weiterarbeiten
Currying
Der λ-Kalkül gestattet nur die Definition einstelliger Funktionen. In Scheme haben wir darüber hinaus nullstellige, mehrstellige und variabelstellige Prozeduren kennen gelernt.
Um mehrstellige Prozeduren auf einstellige zurückzuführen, greifen wir die Idee der Prozeduren höherer Ordnung auf:
Diese Technik lässt sich auf beliebige n-stellige Prozeduren erweitern. Sie bezeichnet man als Currying oder Curryfication, benannt nach dem US-amerikanischen Logiker und Mathematiker Haskell Brooks Curry (* 12. September 1900; † 1. September 1982).
Y-combinator
Die Sonderform define ist im λ-Kalkül ebenfalls nicht vorgesehen.
Zunächst scheint das kein Problem zu sein, da in Scheme unbenannte Prozeduren zur Anwendung kommen können. Doch wie lassen sich dann rekursive Prozeduren definieren?
Wir benötigen dazu eine spezielle Funktion $Y$, die als "Rekursivmacher" fungiert.
Von einer derartigen Funktion muss die sogenannte Fixpunkt-Eigenschaft erfüllt werden:
$(Y \; f) = (f \; (Y \; f))$
Ohne an dieser Stelle den Nachweis zu führen, erfüllt die Definition des Y-combinators diese Forderung:
Wir nutzen zunächst die Kurzform Y zur rekursiven Definition der Fakultätsfunktion:
Natürlich lässt sich diese Fakultätsfunktion auch anwenden. Wir berechnen z.B. $5!=120$:
Abschließend ersetzen wir Y durch den entsprechenden λ-Ausdruck. Nun benötigen wir für rekursive Definitionen tatsächlich kein define!
