Bevor ich garnichts lerne…

Bevor ich garnichts lerne, befolge ich den Ratschlag eines Bekannten, und Blogge über den Stoff, den ich eigentlich lernen sollte. Vielleicht ist das immernoch das Beste, und es bereitet mir weniger Unlust, als jetzt nur zu lesen – und könnte anderen Leuten vielleicht ein gutes Nachschlagewerk produzieren. Wer immer dies hier liest: Es ist eine ziemliche Kurzfassung, kann also durchaus sein, dass einiges für jemanden, für den es neu ist, unverständlich ist. Sollte es wirklich jemanden interessieren, so möge er nachfragen.

Aaalso: Es geht um den Lambda-Kalkül. Um „Lambda“ nicht immer ausschreiben zu müssen, gibt es ein Zeichen – λ.

Das Wichtigste: λ ist ein Dinosaurier.

Zuerst mal was zur Syntax: Aaalso: In der gängigen Mathematik drückt man den Fakt, dass eine funktion f x auf y abbildet aus durch f:x↦y, zum Beispiel f:x↦x+1. Diesen Sachverhalt drückt man im Lambdakalkül aus durch f=λx.y, also z.B. f=λx.x+1. Die Anwendung einer Funktion auf eine Variable oder einen Wert drückt man in der Mathematik aus durch f(x), im Lamdakalkül einfach durch fx.

Zentrale Philosophie des ungetypten Lambda-Kalküls: Alles ist Funktion. Funktionen werden nur Funktionen übergeben, und Funktionen liefern Funktionen zurück. Beispiele sind λx.x – die identische Funktion – oder λf.λx.fx – die Funktion, die einer Funktion f und einer variable x die Applikation fx zuordnet.

Induktiv definiert man die Sprache Λ der korrekten λ-Terme durch folgende Grammatik:

Var ::= x1 | x2 | …

Term ::= Var | (Term Term) |  λ Var . (Term)

W0bei alles, was auf „Term“ passt, in Λ ist. Was auf Var passt, nennt man Variablen. Wir schreiben der Übersichtlichkeit halber aber auch andere Buchstaben dafür. Auch sieht die Definition immer nur Klammern vor – wir lassen sie, wenn wir das Zeug ausschreiben, weg, wo es eindeutig ist. Dabei wird vereinbart, dass Lambda-Abstraktionen stärker binden, als Applikationen, und Applikationen linksassoziativ sind. Abkürzend steht außerdem λabc … .t für λa.λb.λc…t.

Die Menge FV(t) der Freien Variablen eines Terms, das heißt der Variablen, die nie durch ein Lambda gebunden werden, ist induktiv wie folgt definiert:

FV(x) = {x} für Variablen x. FV(rs)=FV(r)∪FV(s) für Terme r, s. FV(λx.t)=FV(t){x}.

Substitution, das heißt Einsetzung in eine Variable, ist definiert durch

x[s/x] = s für x Variable. y[s/x]=y, für y Variable, y≠x. (rt)[s/x]=r[s/x]t[s/x]. (λy.t)[s/x]=λy.t[s/x] falls y∉FV(t) und y≠x. (λx.t)[s/x]=λy.t[y/x] mit einem y∉FV(t), y≠x. (Hoffentlich ist das jetzt richtig…)

Die Kompatible bzw. Kongruente Hülle R‘ einer Relation R ist gegeben durch

xRy ⊢ xR’y, rR’s ⊢ rtR’st, rR’s ⊢ trR’ts, rR’s ⊢λx.rR’λx.s

Eine Relation, die ihre eigene Kompatible Hülle ist, heißt kompatibel.

Die Reflexive Hülle R‘ einer Relation R ist gegeben durch

xRy ⊢ xR’y, ⊢xR’x

Eine Relation, die ihre eigene reflexive Hülle ist, heißt reflexiv.

Die Transitive Hülle R‘ von R ist gegeben durch

xRy ⊢ xR’y, xR’y & yR’z ⊢ xR’z

Eine Relation, die ihre eigene transitive Hülle ist, heißt transitiv.

Die Symmetrische Hülle R‘ von R ist gegeben durch

xRy ⊢ xR’y, xRy ⊢ yR’x

Eine Relation, die ihre eigene symmetrische Hülle ist, heißt symmetrisch.

Die α-Äquivalenz zwischen Termen, geschrieben =α, ist die reflexive, transitive, kompatible, symmetrische Hülle der Relation, die durch die folgende Regel gegeben ist:

⊢ λx.t =α λy.t[y/x], falls y∉FV(t).

Die Barendregt’sche Variablenkonvention besagt nun, dass Alphaäquivalente Terme identifiziert werden sollen, und wir legen fest, dass in Termen gebundene Variablen stets von freien Variablen verschieden sein sollen – dies ist keine Einschränkung, denn Alphaäquivalente Terme besagen offensichtlich dasselbe.

Die Beta-Reduktion →β ist definiert als die kompatible Hülle von

⊢ (λx.t)s →β t[s/x]

Die Beta-Äquivalenz =β ist definiert als die reflexive, transitive Hülle von →β.

Eine Relation R hat die Diamant-Eigenschaft, wenn gilt ∀xyz. xRy∧ xRz → ∃t. yRt ∧ zRt

Eine Relation R heißt lokal konfluent, wenn gilt ∀xyz. xRy∧ xRz → ∃t. yR*t ∧ zR*t

Ein Relation R heißt konfluent, wenn R* die Diamanteigenschaft hat.

Aus Konfluenz folgt offensichtlich die lokale Konfluenz. Umgekehrt ist dies nicht der Fall, wie das Gegenbeispiel {(1,2), (2,3), (3,2), (3,4)} zeigt.

β ist lokal konfluent. Beweis: Sei x→β y∧ x→β z. Wir unterscheiden nach dem Aufbau des Terms x: x kann keine Variable sein, denn eine Variable ist nicht reduzierbar. ist x=λa.t, so ist y=λa.u und z=λa.v, also t→β u und t→β v, also nach Induktionsvoraussetzung existiert ein w, sodass u→β*w und v→β*w, also auch t→β *w, also auch x→β * λa.w. Der Fall x=rs teilt sich in die Unterfälle nach r auf. Er sei dem gewandten Leser überlassen (keine Lust, den jetzt aufzuschreiben).

Für den Konfluenzbeweis definieren wir zunächst eine „Hilfsrelation“, die Parallele Reduktion ⇒. Sie ist definiert als die reflexive transitive kompatible Hülle von

t⇒t‘ & s⇒s‘ ⊢ (λx.t)s⇒t'[s’/x]

Trivialerweise kann man mit ⇒ alles ableiten, was man mit →β ableiten kann. Umgekehrt ebenfalls, da ein ⇒-Schritt lediglich mehreren →β-Schritten gleichkommt, also ⇒* = →β *.

Die Vollständige Entwicklung t* eines Terms hat leider dieselbe Notation wie R* zu einer Relation R, hat aber damit nichts zu tun. Sie ist definiert durch

((λx.t)s)* = t*[s*/x], (rs)*=r*s*, (λx.t)*=λx.t*, x*=x

In ihr werden alle sichtbaren Redexe (also alle Teile, die man Betareduzieren kann), entfernt. Offensichtlich ist die vollständige Entwicklung eindeutig. Ist r⇒s, so ist s⇒r* – dies ist ein Lemma, das man induktiv beweisen kann. Daraus folgt unmittelbar, dass ⇒ die Diamanteigenschaft hat. Damit ist ⇒ auch konfluent, also hat ⇒* die Diamanteigenschaft, also auch →β *, also ist auch →β konfluent.

Sei → eine Relation. Wir definieren t∈nf(→) :⇔ ¬∃u. t→u. Statt nf(→β) schreiben wir einfach nf. Ein Element von nf heißt Normalform. Da die Betareduktion konfluent ist, sind Normalformen eindeutig.

Ein Term der Gestalt x{a}, wobei {a} für die Zeichenkette a1 a2 … an stehe (normalerweise verwendet man dafür Vektornotation, geht aber mit Unicode wohl nicht), heißt blockiert. Eine Abstraktion  λx.t heißt schwacher Kopfwert. Blockierte Terme und Abstraktionen heißen Schwache Kopfnormalformen. Alle Anderen terme besitzen einen Schwachen Kopfredex (λx.t)a{a}. Schwache Kopfreduktion ist definiert als

⊢ (λx.t)a →wh t[a/x], r →wh r‘ ⊢ rs →wh r’s

Kopfnormalformen sind Terme der Gestalt λ{a}.x{b}. Kopfredexe haben die Gestalt λ{a}.(λx.t)b{b}. Kopfreduktion ist definiert durch

a →wh t ⊢ a →ht, t→ht‘ ⊢λx.t→hλx.t

Standardreduktion ist definiert durch

t→wh t‘ & t‘ →st“ ⊢t →st“, s→ss‘ & r→sr‘ ⊢ rs→sr’s‘, ⊢x→s für Variablen x, t →st’⊢λx.t →sλx.t‘

Es gilt t→st’⇔t→β *t‘, der Beweis ist eher länglich.

So, soweit mal bis hierher. Wahrscheinlich schreib ich heut Abend noch was. Oder auch nicht. Je nachdem, wie ich grad drauf bin.

Schreibe einen Kommentar

Trage deine Daten unten ein oder klicke ein Icon um dich einzuloggen:

WordPress.com-Logo

Du kommentierst mit Deinem WordPress.com-Konto. Abmelden / Ändern )

Twitter-Bild

Du kommentierst mit Deinem Twitter-Konto. Abmelden / Ändern )

Facebook-Foto

Du kommentierst mit Deinem Facebook-Konto. Abmelden / Ändern )

Google+ Foto

Du kommentierst mit Deinem Google+-Konto. Abmelden / Ändern )

Verbinde mit %s

%d Bloggern gefällt das: