Der Lambda-Kalkül

Der Lambda-Kalkül  

Notation

Ein Ausdruck (Term) des Lambda-Kalküls setzt sich allein aus folgenden Teilen zusammen:

1. Ein Variablenname

2. Ein sog. Lambda-Ausdruck

3. Eine Funktionsanwendung

Aus diesen drei Komponenten und ein paar Klammern zum Gruppieren lässt sich, wie wir sehen werden, jedes beliebige Programm notieren! Betrachten wir die Terme einmal einzeln:

Ein Variablenname kann wie in uns bekannten Programmiersprachen ein beliebiges Wort und tut genau das, was wir erwarten. Er sieht z.B. so aus:

x

Interessanter ist da dieser ominöse Lambda-Ausdruck . Wir notieren ihn folgendermaßen:

\x . Term

wobei der Backslash dem griechischen Buchstaben Lambda (namensgebend für unseren gesamten Kalkül), nachempfunden ist. Der Lambda-Ausdruck steht für nichts anderes als eine anonyme Funktion mit einem Parameter (hier x), die den Ausdruck auf der rechten Seite des Punktes zurückgibt. Solche Funktionen kennen wir selbst aus VB. Dort würden wir schreiben

Function(x) Term

Tatsächlich wird sogar auch diese Art von Ausdruck oft als lambda expression bezeichnet und in Python schriebe man in Anlehnung daran

lambda x: term

Nun fehlt noch die Funktionsanwendung (Applikation). Was man mathematisch als f(x) notiert, schreiben wir schlicht als

f x

Das soll die komplette Grundlage für jede Berechnung sein? Man kann Funktionen erzeugen und wieder auswerten, aber wie soll man etwas interessantes tun? Wir werden sehen ...

Auswertungsregeln

Nun, da die Frage der Notation geklärt ist, geht es darum, wie wir mit den verschiedenen Termen rechnen können. Wir bezeichnen das als Auswerten. Betrachten wir z.B. den Term

(\x . x) y

dann besteht der aus einem Lambda-Ausdruck und einer Anwendung. In VB wäre das

(Function(x) x)(y)

und wir führen die Funktionsanwendung einfach durch, ersetzen also den Parameter x durch das Argument y. Genau können wir den Ausdruck (\x . x) y zu y auswerten. Wenn ein Term durch Auswerten aus einem anderen hervorgeht, so heißen die beiden äquivalent und ich notiere das mit einem ==. Das Ergebnis von oben kann ich also festhalten als

(\x . x) y == y 

Nun ein anderes Beispiel:

(\x . c) y == c

Hier wird y im Lambda-Ausdruck nicht verwendet, spielt also keine Rolle für das Ergebnis.

Eine Auswertung kann natürlich auch mehrere Schritte benötigen, aber auch dann wird einfach der Reihe nach eingesetzt:

(\f . f p) (\x . x) 
== (\x . x) p
== p

Es ist wichtig festzustellen, dass wir Funktionen (etwas anderes sind ja Lambda-Ausdrücke nicht) offenbar problemlos als Argumente an andere Funktionen übergeben oder als Rückgabewerte erhalten können. Das war's auch schon zu den Auswertungsregeln - man muss lediglich aufpassen, dass ein Einsetzen niemals den Sinn eines Ausdrucks verändert (nicht umsonst stehen hier Gleichheitszeichen). Ein Beispiel für eine solche Situation.

(\x . (\y . y x)) y == \y . y y

Diese Auswertung ist falsch, denn das y innerhalb des Lambda-Ausdrucks und das y außerhalb sind nicht die selbe Variable - die eine ist im Ausdruck gebunden, die andere frei. Das Problem wird deutlicher, wenn wir den Term mit einer anderen Variablen auswerten.

(\x . (\y . y x)) z == \y . y z

Der obige Term ist natürlich von unserer falschen Auswertung verschieden. Er übergibt der Funktion y den Wert von z und nicht etwa sich selbst. Um diesen Fehler also systematisch zu vermeiden, müssen wir manchmal den Parameter eines Lambda-Ausdruckes umbenennen! Das ändert nie dessen Inhalt:

(\x . (\y . y x)) y
== (\x . (\z . z x)) y
== \z . z y

Wer hier und im Folgenden experimentieren möchte, der kann gleich das Beispielprogramm zu diesem Tutorial starten und mittesten .

So weit, so gut. Das sieht jetzt zwar alles ganz nett aus und man kann zugegebenermaßen sehr kompakt Funktionen notieren, aber wie und womit sollen wir rechnen? Beim Rechnen braucht man doch irgendwelche Zahlen, Formeln und Schleifen?

Tatsächlich halte ich das Versprechen, dass man mit nichts als den obigen Definitionen alles berechnen kann. Also mit Funktionen rechnen? Das geht - und in den nächten Kapiteln geht es darum, wie man sich alles, was man zum herkömmlichen Programmieren braucht, Schritt für Schritt mit ein paar Lambdas schaffen kann.

Church-Encoding  

In diesem Teil basteln wir uns aus den "nackten" Lambda-Termen bessere Kontroll- und Datenstrukturen. Als erste Hilfe betrachten wir

Mehrere Parameter

Bis jetzt haben unsere Funktionen immer nur einen Parameter. Nichts anderes ist offenbar von der Definition vorgesehen, aber das genügt auch. Angenommen, wir hätten einen Additionsoperator `+' (wie wir ihn später entwickeln werden) und wollten eine Funktion schreiben, die ihr Argument um 1 erhöht. Klar:

\b . b + 1

Und um 3?

\b . b + 3

Und nun um n? Dazu verwenden wir eine weitere Funktion

\n . (\b . b + n)

Diese können wir nun wieder spezialisieren, indem wir für n etwas einsetzen.

(\n . (\b . b + n)) 3 == \b . b + 3

Und wenn wir auf das Ergebnis wieder etwas anwenden?

((\n . (\b . b + n)) 3) 4
== (\b . b + 3) 4 
== 4 + 3
== 7

Funktioniert! Wir können also Funktionen mit mehreren Parametern als einfache Funktionen schreiben, die neue Funktionen zurückgeben, und wenden beim Einsetzen einfach mehrere Applikationen an (diese Technik heißt Currying). Weil man das so häufig braucht, führt man ein paar syntaktische Vereinfachungen ein und erlaubt Lambdas mit mehreren Parametern

\a b . c == \a . \b . c

Bei der Auswertung ist

f a b == (f a) b

Noch ein Beispiel für die Praxis ...

(\a b . f a b) x y
== ((\a . \b . f a b) x) y
== (\b . f x b) y
== f x y

Boole'sche Werte

Aber jetzt haben wir ja nur wieder an Funktionen herumdefiniert - wir wollten doch rechnen und dazu braucht man die entsprechenden Datentypen. Die Art und Weise, mit der man gängige Datenstrukturen rein durch Lambda-Funktionen nachbildet, nennt sich nach ihrem Erfinder Church-Encoding . Als erstes Beispiel beginnen wir mit Wahrheitswerten (True/False). Man definiert diese folgendermaßen:

True ist eine Funktion, die aus zwei Argumenten das erste zurückgibt, False das zweite.

Oder auch

true  := \a b . a
false := \a b . b

Das := verstehe ich einfach als Textersetzung, so dass man überall, wo wir true benutzen, diese Definition einsetzen könnte.

Das sieht doch recht einfach aus. Mit dieser Definition von Wahrheitswerten haben wir sogar If/Then/Else schon abgedeckt. Der Code

bedingung Juhu Nein

gibt genau dann Juhu zurück, wenn die Bedingung true ist, andernfalls Nein. Beweis:

true  Juhu Nein == (\a b . a) Juhu Nein == (\b . Juhu) Nein == Juhu
false Juhu Nein == (\a b . b) Juhu Nein == (\b .    b) Nein == Nein

Jetzt fehlen nur noch ein paar bool'sche Operatoren, um die Wahrheitswerte zu verknüpfen.

not := \w . w false true
and := \p q . p q false
or  := \p q . p true q

Ein paar Beispiele für logische Rechnungen

not false 
== (\w . w false true) (\a b . b)
== (\a b . b) false true
== true

or false (not true) 
== (\p q . p true q) false false
== (\p q . p true q) (\a b . b) false
== (\a b . b) true false
== false

Man kann sich übrigens genauso das Konstrukt

if cond then a else b

zurechtbasteln, wobei if eine Funktion mit 5 Argumenten ist. Das ist reine Optik.

Tupel

Ein Tupel (a,b) ist ein Verbund aus mehreren Werten, der einem u.A. hilft, wenn eine Funktion mehr als einen Rückgabewert haben soll, ähnlich wie die zwei Koordinaten eines Punktes. Ein Tupel mit Lambdas zu definieren, ist nicht allzu schwierig. Natürlich ist es eine Funktion und dieser muss man nur mitteilen, ob sie einem den ersten oder zweiten gespeicherten Wert liefern soll.

(a, b) := \w . w a b

Einen Wert für w, der uns gerade a bzw. b liefert, sind z.B. die Funktionen true und false, so dass wir Hilfsfunktionen anbieten:

first  := \tupel . tupel true
second := \tupel . tupel false

Beispiel:

zahlUndQuadrat := \n . \w . w n (n * n)

zahlUndQuadrat 3 == \w . w 3 9
first  (zahlUndQuadrat 3)  == (\w . w 3 9) (\a b . a) == (\a b . a) 3 9 == 3
second (zahlUndQuadrat 3)  == (\w . w 3 9) (\a b . b) == (\a b . b) 3 9 == 9

Zahlen

Endlich, nachdem wir gesehen haben, dass man tatsächlich Datenstrukturen, die nichts mit Funktionen zu tun haben, durch diese definieren kann, können wir uns auch an Zahlen wagen. Wir definieren

0 := \f x . x
1 := \f x . f x
2 := \f x . f (f x)
3 := \f x . f (f (f x))
...

Eine Zahl n ist also wieder eine Funktion, und zwar eine, die eine gegebene weitere Funktion genau n mal hintereinander auf einen Wert anwendet. Das klingt sperrig, allerdings kann man so arithmetische Operatoren sehr leicht definieren. Die Addition muss einfach die Funktionen von beiden Summanden hintereinanderverketten.

+ := \a b . \f x . a f (b f x) 

(+ 2 1)
== (\a b . \f x . a f (b f x)) 2 1
== \f x . 2 f (1 f x)
== \f x . f (f (1 f x))
== \f x . f (f (f x))
== 3

Und darauf aufbauend entstehen weitere Operatoren - Multiplikation wird beispielsweise als sich wiederholende Summierung geschrieben.

* := \a b . a (+ b) 0

(* 2 2)
== 2 (+ 2) 0
== (+ 2) ((+ 2) 0)
== (+ 2) 2
== 4

Der Ausdruck (+ 2) ist dabei durch das Currying möglich - Zur Erinnerung:

+ a b == (+ a) b

Weiterhin kann man die üblichen Vergleichsfunktionen auf Nullheit (Funktion wird nie ausgeführt) und Gleichheit definieren:

zero? := \n . n (\x . false) true
=     := \a b . zero? (- a b)

(= 3 3) 
== zero? (- 3 3)
== zero? 0
== (\n . n (\x . false) true) (\f x . x)
== (\f x . x) (\x . false) true
== true

Ich gehe an dieser Stelle nicht weiter auf das Church-Encoding ein, es ist aber möglich, in analoger Weise Tupel zu Listen beliebiger Länge, zu Bäumen, Bruchzahlen, Strings etc. auszubauen ...

Schleifen  

Wunderbar - An Datenstrukturen scheint es uns nicht mehr zu mangeln. Doch ein ungelöstes Problem gibt es noch. Mit dem bisschen Einsetzen ist man ja recht schnell fertig - nach einer langen und aufwändigen Berechnung sah noch nichts aus. Wie denn auch? Wir kennen keine Möglichkeit, dass sich irgendetwas wiederholt, also in Schleife ausgeführt wird.

Tatsächlich gibt es im Lambda-Kalkül keine Schleifen, dass aber langwierige, sich widerholende Berechnungen beschreibbar sind, kann schnell durch diesen interessanten Term gezeigt werden.

(\x . x x) (\x . x x)

Versuchen wir einmal, ihn auszuwerten:

(\x . x x) (\x . x x)
== (\x . x x) (\x . x x)
== (\x . x x) (\x . x x) ??

Was ist das jetzt? Es geht nicht! Der Term reduziert sich durch Einsetzen zu sich selbst - wir haben eine Art Endlosschleife in der Auswertung geschaffen. Es gibt also noch Hoffnung, doch noch irgendetwas schleifenartiges in die Hände zu bekommen. Wenn es keine Iteration gibt ... gibt's ja immer noch Rekursion - Eine Funktion, die sich selbst aufruft. Probieren wir uns doch einmal an einer Funktion, die uns alle Zahlen von 1 bis n summiert:

Function Sum(n)
    If n = 0 Then
        Return 0
    Else
        Return n + sum(n - 1)
    End If
End Function

Vielleicht kommen wir ja so weiter:

sum := \n . if (zero? n) then 0 else (+ n (sum (- n 1)))

Sieht gut aus, funktioniert aber nicht. Wir müssen ja jederzeit sum durch die Definition auf der rechten Seite ersetzen können.

Hmm, da steht ja immernoch ein sum. Offenbar können wir einfach keine rekursiven Funktionen schreiben! Irgendwie klar - der einzige Mechanismus zur Funktionsdefinition ist ja das Lambda, das eine anonyme Funktion schafft. Und eine anonyme Funktion hat ja nun keinen Namen, über den man sie rekursiv aufrufen könnte.

Man schafft es aber tatsächlich, in einem nichtrekursiven System wie dem Lambda-Kalkül jede Menge Rekursionen zu erzeugen. Wie das genau geht, ist höchst interessant aber auch verzwickt, es ist daher kein Problem, wenn der folgende Abschnitt nur überflogen wird. Ich probiere es dennoch kleinschrittig ...

Die Idee der Rekursion bringt uns in die richtige Richtung - wir müssen nur noch einen kleinen Umweg gehen. Wenn die Funktion nicht auf sich selbst zurückgreifen kann, dann kann man ihr ja wenigens eine Funktion als Argument gönnen, die sie statt dessen aufruft. Diesen nicht-rekursiven Prototyp nennen wir einmal sumf.

sumf := \rec n . if (zero? n) then 0 else (+ n (rec (- n 1))) 

Ohne Frage: Das geht. Aber wir können sumf immer noch nicht sinnvoll aufrufen, denn was sollen wir ihr für den rekursiven Aufruf übergeben? Gut, machen wir ein Gedankenexperiment und nehmen an, wir hätten schon unsere funktionierende Summenfunktion sum. Wenn wir diese für den rekursiven Aufruf übergeben, wird auch sumf sicherlich richtig funktionieren.

sumf sum 
== (\rec n . if (zero? n) then 0 else (+ n (rec (- n 1)))) sum 
==  \n . if (zero? n) then 0 else (+ n (sum (- n 1)))

Holla, das Ergebnis dieses Aufrufs ist also wieder unsere funktionierende Summenfunktion. Da wir die ja schon "haben", können wir beides gleichsetzen.

sum == sumf sum

Und nun kommt der entscheidende Schritt - Nehmen wir an, es existiere eine Zauberfunktion Y, der man unseren Prototypen übergibt und die daraus die korrekt rekursive Funktion sum berechnet. Mit dieser könnte man also sagen

sum == Y sumf

Andererseits ist aber sumf sum == sum, also

sumf sum == Y sumf

... und durch die 2. Definition:

sumf (Y sumf) == Y sumf.

Was hat uns jetzt diese Rechnerei gebracht? Durch Umstellen und Umbenennen kriegen wir eine Gleichung, die die Anforderungen an unsere Wunderfunktion Y spezifiziert. Für jede Prototypenfunktion f gilt dann nämlich

Y f == f (Y f)

und das Ergebnis ist die fertige rekursive Funktion. Nun müssen wir nur noch eine Funktion finden, die diese Gleichung erfüllt.

Die Lösung finden wir in einer Verallgemeinerung der Endlosschleife vom Anfang des Kapitels - Sie lautet:

Y := \f . (\x . f (x x)) (\x . f (x x)) 

Mit Beweis:

Y f 
== (\x . f (x x)) (\x . f (x x))
== f ((\x . f (x x)) (\x . f (x x)))
== f (Y f)

Perfekt! Diese Wunderfunktion enthält nun keine Magie, erfüllt aber alle Erwartungen! Nun endlich ist jede Rekursion möglich und damit die Summenfunktion kein Thema mehr.

sum := Y (\sum n . if (zero? n) then 0 else (+ n (sum (- n 1))))

Diese Definition ist wohlgemerkt nicht rekursiv, weil das sum auf der rechten Seite nur der Parameter des Lambda-Ausdruckes ist und genau so gut rec etc. heißen könnte.

Dies ist im Grunde der faszinierendste Zug des Lambda-Kalküls. Ein System, das über keinen Iterationsmechanismus und keine Rekusion verfügt, kann dennoch eine solche durchführen. Die Möglichkeiten, die uns die Y-Funktion (der sog. Fixpunktkombinator) liefert, sind endlos.

Zum Abschluss noch ein Wort zur Endlosschleife: In VB könnten wir bestimmt eine durch folgenden Code provozieren

Function a()
    Return a()
End Function

Das wäre die rekursive Funktion a := a, was wir mit dem Y-Kombinator schreiben können als

a := Y (\a . a)

Indem wir das in Y einsetzen, bekommen wir genau das Beispiel

a = (\x . x x)(\x . x x)

vom Anfang des Kapitels!

Praktisches Lambda-Kalkül  

Wir waren nun lange genug dabei, die theoretischen Möglichkeiten des Lambda-Kalküls auszuloten. Die erste Möglichkeit, ein Gefühl für die Sprache zu bekommen, ist sie zu

Testen

ganz interaktiv mit dem Beispielprogramm . Eingeben und auswerten.

Diese Funktion ist hauptsächlich dazu gedacht, die Auswertungsregeln zu verstehen und nicht, um wirklich zu rechnen. Dazu brauchen wir noch

Strikte Auswertung  

Wir haben gesehen, wie aus der reinen Basis der Lambda-Ausdrücke Datenstrukturen, Konstrollstrukturen und Syntaxelemente entstehen. Bietet es sich nicht an, das Ganze zu einer echten Programmiersprache weiterzuentwickeln? Nun ja, eine Kleinigkeit fehlt. Programmiersprachen, wie wir sie gewohnt sind, werten nach einem strikten Muster aus. Sage ich in VB

Call MsgBox(prompt())

so wird zunächst die innere Funktion ausgewertet und dann die MessageBox aufgerufen. Diese natürliche Reihenfolge ist im Lambda-Kalkül nicht unbedingt gegeben und stellenweise sogar schädlich.

Betrachten wir den Term

if false then (Y (\a . a)) else 1

Logisch ergibt das 1, würde man jedoch strikt auswerten, müssten zunächst alle Argumente der if-Funktion ausgerechnet werden, darunter auch die berüchtigte Endlosschleife. Die korrekte Funktionsweise des Programmes hängt also entscheidend davon ab, dass hier nicht strikt ausgewertet wird.

In einer echten Programmiersprache möchten wir aber i.d.R. (siehe nächstes Kapitel) strikte Auswertung. Das erlaubt uns sogar, einen einfacheren Compiler zu schreiben, wir müssen aber Programme manchmal etwas umformulieren, damit sie auch strikt funktionieren. Im obigen Beispiel schriebe man

iff bedingung then (\_. wahr) else (\_. falsch) 

Die Argumente vom strikten iff sind hier Dummy-Funktionen, die die Auswertung zunächst verhindern.

Wo landet man nun mit striktem Lambda-Calculus? Ganz klar, wir können den Code 1:1 in eine Sprache wie JavaScript oder Python übersetzen.

Aus

(\x y . x) 1 2 

wird

((lambda x : lambda y : x)(1))(2)

Wir können genauso trivial einen Interpreter für diese Sprache selbst schreiben, sie besteht ja nur aus zwei Konstrukten! Um dann eine richtige Programmiersprache zu erhalten, müssen wir nur noch Bibliotheken und ein paar syntaktische Feinheiten liefern.

Wichtig sind z.B. lokale Zuweisungen der Form

let x = rechnung 
  in f x

die wir leicht umschreiben können als

(\x . f x) rechnung

aber deutlich leicher zu lesen sind. Die entstehende Programmiersprache liest sich so:

let isPrime = (\n . 
    let divisors = range 2 (- n 1) in
    all (\d . (!= 0 (mod n d))) divisors) in

let primes = (\max . filter isPrime (range 2 max)) in

length (primes 100)

Was haben wir gewonnen? Eine leicht zu implementierende und extrem mächtige Programmiersprache, die Funktionen, Funktionsobjekte, Kapselung und komplizierte Datenstrukturen automatisch beherrscht (und sich nebenbei in Javascript-Einzeiler kompilieren lässt).

Ausblick: Typsystem  

Eine Sache fehlt noch, um aus einer spannenden Sprache eine ernstzunehmende Sprache zu machen. Im Moment bestehen alle Objekte unserer Sprache aus Lambda-Funktionen, es ist unvermeidlich, sie irgendwann falsch aufzurufen und dann mehr oder weniger unmöglich, das Ganze zu debuggen. Es müsste eine Möglichkeit geben, sinnvollen Code automatisch von unlogischem Code zu unterscheiden: Ein Typsystem muss her . Die einfachen Typen sind ja wie immer, man könnte sagen

numElements :: Int
numElements := 42

Auch für einfache Lambda-Ausdrücke ist ein Typ schnell gefunden

inc :: Int -> Int
inc := (+ 1)

Für Funktionen mit mehreren Argumenten ergibt sich nach der Currying-Logik

plus :: Int -> Int -> Int
plus := \a b . (+ a b)

plus 1 :: Int -> Int
plus 1 2 :: Int

Für manche Ausdrücke ist der Typ aber weniger klar. Was machen wir z.B. mit \x . x? Offenbar gibt der Ausdrück für jeden Typen a wieder etwas dieses Typs zurück. Man braucht also Typvariablen der Art

identity :: a -> a
identity := \x . x

Was wäre das in VB? Richtig:

Function Identity(Of T)(x as T) As T
    Return x
End Function

Ein paar Beispiele für kompliziertere Signaturen (wie Listenoperationen)

z :: [a] -> [b] -> [(a,b)]
m :: (a -> b) -> [a] -> [b]

Preisfrage: Was könnten diese Funktionen tun?

Es ist übrigens möglich, typisierte Programme zu schreiben, ohne auch nur einen der Typen selbst anzugeben! Ist das Typsystem ausgereift genug, so kann man sagen: Kompiliert das Programm überhaupt, ist es höchstwahrscheinlich korrekt.

Fügt man zu unserem verfeinerten, strikten Lambda-Kalkül nun ein Typsystem hinzu, so kommt man ganz nah bei F# heraus. Verfeinert man das Typsystem noch weiter und wirft (mit größter Vorsicht) die strikte Auswertung wieder über Bord, so hat man Haskell .

Demoprogramm  

Download Demoprogramm (Ausführbar+Source, geschrieben in F#)

Befehlszeile:

                     : Interaktivmodus
         <dateiname> : Ausführen, Ergebnis als Church-Zahl ausgeben
-compile <dateiname> : Syntaxzucker entfernen (klassischer LC)
-classic <dateiname> : Klassisches LC-Skript ausführen
-js      <dateiname> : Nach HTML/Javascript kompilieren

Ihre Meinung  

Falls Sie Fragen zu diesem Artikel haben oder Ihre Erfahrung mit anderen Nutzern austauschen möchten, dann teilen Sie uns diese bitte in einem der unten vorhandenen Themen oder über einen neuen Beitrag mit. Hierzu können sie einfach einen Beitrag in einem zum Thema passenden Forum anlegen, welcher automatisch mit dieser Seite verknüpft wird.