Aufriß des Lambda-Kalküls (in Lisp-Notation)

Der Lambda-Kalkül als formallogische Abstraktion dessen, was Algorithmen sind, was sie leisten, wozu sie fähig sind und wozu nicht, bedient sich einer suggestiven Notation, die anders als die ebenso abstrakte Modellbildung durch die Turing-Maschine(n) alle algorithmischen Abläufe mathematisch-symbolisch (re‑)konstruiert, statt codierte Programme auf einer virtuellen Maschine (quasi‑)prozedural zu implementieren. Im Lambda-Kalkül wird der mathematische Kern von Algorithmen in die formale Symbolik selbst ‘eingelagert’ oder ‘eingebaut’, bei der Turing-Maschine wird der mathematische Sinn von Algorithmen in einen separaten Code ‘übertragen’ oder ‘übersetzt’. Es erinnert in gewisser Weise an die subtile, letztlich illusorische Differenz, wie sie zwischen einem Interpreter und einem Compiler entsteht, obwohl in beiden Fällen mit einer durchformalisierten Sprache gearbeitet wird, um ein ausführbares Programm zu schreiben. Die Modellierung abstrakter Strukturen durch den Lambda-Kalkül einerseits und durch die Turing-Maschine(n) andererseits erweckt den Eindruck, als sei, um es scholastisch auszudrücken, zwischen intentio recta und intentio obliqua zu unterscheiden. Wie gesagt, es handelt sich um eine Illusion, die allerdings alles andere als abwegig ist.

Wird von der üblichen Punkt-Notation des Lambda-Kalküls abgewichen, um sich den symbolischen Kalkül in Lisp-Notation anzusehen, hat das seinen eigenen Reiz, weil sich das funktionale/prozedurale Konzept in aller Unmittelbarkeit abzeichnet, wenn man mit Lisp oder Scheme vertraut ist. Daß sich die Lisp-Notation anbietet, um den Lambda-Kalkül, wie er von Alonzo Church konzipiert wurde, im Aufriß darzustellen, liegt daran, daß die Symbolik von Lisp (oder Scheme) eben daher stammt (mutatis mutandis). Es ergibt sich folgendes Bild:

Terme, Applikation und λ‑Abstraktion

  • Terme sind Variable wie a, b, c, … x, y, z, …, die als elementare Terme gelten, sowie
  • komplexe Terme der Gestalt (P Q) oder (λ (vQ), wobei P und Q (irgendwelche) Terme sind, und v (irgend‑) eine Variable ist.
  • Ein Term der Gestalt (P Q) heißt Applikation (des Operators P auf den Operanden Q).
  • Und ein Term der Gestalt (λ (vQ) heißt λ‑Abstraktion (oder einfach Abstraktion); wobei λ ein reserviertes Symbol des danach benannten Lambda-Kalküls ist.

Formeln

Als Formel gelten

  • Reduktion P → Q
  • Äquivalenz P = Q

wobei P und Q Terme sind.

Klammern (syntactic sugar)

  • Bei einer geschachtelten Applikation kann eine linksassoziative Klammerung unterdrückt und ein Term der Gestalt ((P QR) als (P Q R) geschrieben werden.
  • Eine geschachtelte Abstraktion der Gestalt (λ (u) (λ (vQ)) kann abgekürzt durch den Ausdruck (λ (u vQ) wiedergegeben werden, und entsprechend zu verstehen sind Ausdrücke wie (λ (u v wQ), (λ (u v w xQ) etc.

Freie vs. gebundene Variable

Eine Variable v, die im Term Q vorkommt, wird (darin) frei genannt, falls sie nicht im Geltungsbereich einer λ‑Abstraktion (λ (v) …) liegt, die einen (Sub‑) Term von Q bildet; andernfalls wird jene Variable als gebunden bezeichnet.

Umbenennung

Die Notation {y/x}Q steht für das Resultat einer (durchgängigen) Umbenennung der Variablen x in y innerhalb des Terms Q, egal ob sie darin frei oder gebunden vorkommt. Tritt die umzubenennende Variable im Term überhaupt nicht auf, bleibt er unverändert.

Substitution

Die Notation [P/x]Q repräsentiert das Resultat, das sich ergibt, wenn innerhalb des Terms Q die Variable x durch den Term P substituiert wird, und zwar überall wo sie darin frei vorkommt. Dabei dürfen allerdings keine freien Variablen des Terms P gebunden werden; zuvor sind deshalb im Term Q jene darin gebunden vorkommenden Variablen gleichen Namens auf geeignete Weise umzubenennen.

Axiome

  1. Q → Q
  2. Transitivität der Reduktion: mit P → Q und Q → R gilt P → R
  3. Mit P → Q gilt (R P) → (R Q)
  4. Mit P → Q gilt (P R) → (Q R)
  5. Mit P → Q gilt (λ (vP) → (λ (vQ)
  6. Reduktion bewahrt Semantik: mit P → Q gilt P = Q
  7. Kommutativität der Äquivalenz: mit P = Q gilt Q = P
  8. Transitivität der Äquivalenz: mit P = Q und Q = R gilt P = R
  9. Beta-Reduktion: ((λ (uQv) → [v/u]Q
  10. Eta-Reduktion: (λ (v) (Q v)) → Q, falls v in Q nicht frei vorkommt

Kalkulation als Reduktion

Unter einer Kalkulation ist eine Sequenz von Termen zu verstehen, die jeweils durch Reduktion auseinander hervorgehen, also etwa P → Q → R → S → T; wobei sich, abgesehen vom Term am Anfang, jeder weitere Term jener Sequenz reduktiv aus dem unmittelbar vorher­gehenden ergibt. Der vorangehende Term bei einer Reduktion wird Redex genannt, und der nachfolgende wird dann als Redukt bezeichnet.

Term vs. Form

Ein Term heißt Form, falls keine freien Variablen darin vorkommen.

Normalform

Ein Term ist in Normalform, falls er keine (Sub‑) Terme der Gestalt ((λ (vPQ) oder (λ (v) (Q v)) enthält. Und daß ein Term eine Normalform hat, heißt: Es gibt eine Kalkulation, die, ausgehend von jenem Term, mit einem Term in Normalform endet.

Church/Rosser-Theorem

Wenn P = Q für zwei Terme P und Q gilt, dann existiert ein Term R, so daß P → R und Q → R gilt.

Korollar:

Wenn ein Term eine Normalform hat, so ist diese eindeutig.

Wert

Die Normalform eines Terms ist als sein Wert zu betrachten. Daher ist, falls der Term überhaupt eine Normalform hat, sein Wert durch Kalkula­tion zu finden. Und jene Kalkulation bricht ab oder terminiert, sobald eine Normalform erreicht ist. Dagegen gibt es bei einem Term ohne Normal­form keine terminierende Kalkulation.

Term ohne Normalform

Wegen

((λ (v) (v v)) (λ (v) (v v)))

→ ((λ (v) (v v)) (λ (v) (v v)))

hat der Term ((λ (v) (v v)) (λ (v) (v v))) keine Normalform.

Fundamentale Definitionen

Identität

id := (λ (uu)

Wahrheitswerte

true := (λ (u vu)

false := (λ (u vv)

Logik-Operatoren

not := (λ (u) (u false true))

and := (λ (u v) (u (v true falsefalse))

or := (λ (u v) (u true (v true false)))

Listen-Operatoren

car := (λ (v) (v true))

cdr := (λ (v) (v false))

cons := (λ (u v w) (w u v))

Natürliche Zahlen

0 := id

n‘ := (cons n true)

Zählen mit Successor,  Predecessor,  Zero-Prädikator

succ := (λ (v) (cons v true))

pred := car

zerop := (λ (v) ((cdr vfalse true))

Dotted-Pair

(P . Q) := (λ (w) (w P Q))

Fixpunkt‑Theorem

Zu jedem Term F existiert ein Term X, Fixpunkt von F genannt, so daß (F X) = X gilt.

Fixpunkt‑Konstruktion

X = ((λ (v) (F (v v))) (λ (v) (F (v v))))

Fixpunkt‑Operator

fxpt := (λ (f v) (f (v v))) (λ (v) (f (v v)))

Exemplarische Kalkulationen

(true id) = false

(true id)

→ ((λ (u vuid)

→ (λ (vid)

→ (λ (v) (λ (ww))

→ (λ (v ww)

→ false

(true P Q) = P

(true P Q)

→ ((λ (u vuP Q)

→ P

(false P Q) = Q

(false P Q)

→ ((λ (u vvP Q)

→ Q

(not true) = false

(not true)

→ ((λ (w) (w false true)) true)

→ (true false true)

→ false

(not false) = true

 (not false)

→ ((λ (w) (w false true)) false)

→ (false false true)

→ true                                                                                                                                                                                (

(not (not true)) = true

(not (not true))

→ (not false)

→ true

(not (not false)) = false

(not (not false))

→ (not true)

→ false

(not not) = (λ (u v w) v)

(not not)

→ (λ (w) (w false true)) (λ (u) (u false true))

→ ((λ (u) (u false true)) false true)

→ ((false false truetrue)

→ (true true)

→ ((λ (x ux) (λ (v wv))

→ (λ (u) (λ (v wv))

→ (λ (u v wv)

(not not true) = true

(not not true)

→ ((λ (u v wvtrue)

→ (λ (v wv)

→ true

[!]    (not not false) = true

(not not false)

→ ((λ (u v wvfalse)

→ (λ (v wv)

→ true

Extensionalität

Seien f und g Funktionen (im mathematisch üblichen Sinne). Wenn f(x) = g(x) für alle x gilt, dann ist f = g.

Beweis (mittels Eta-Reduktion):

Angenommen (P x) = (Q x) gilt für einen Term x, der nicht als freie Variable in den Termen P und Q vorkommt, dann gibt es einen Term T, so daß:

(P x) → T und (Q x) → T

Also:

(λ (x) (P x)) → (λ (x) T)

(λ (x) (Q x)) → (λ (x) T)

(λ (x) (P x)) = (λ (x) T)

(λ (x) (Q x)) = (λ (x) T)

(λ (x) (P x)) = (λ (x) (Q x))

(λ (x) (P x)) → P

(λ (x) (Q x)) → Q

(λ (x) (P x)) = P

(λ (x) (Q x)) = Q

P = Q

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s