Lambda-Kalkül: Die Dritte (und voraussichtlich Letzte)

So. Angekommen sollte ich mich jetzt mentaal vielleicht lieber aufs Schlafen konzentrieren, aber andererseits laufen bei mir erfahrungsgemäß die Prüfungen am Besten, zu denen ich total übermüdet erscheine… Keine Ahnung, warum.

Also mach ich am Besten da weiter, wo ich aufgehört habe. Ich war bei Extensionalität stehengeblieben…

Kommen wir zum Satz von Curry: Betagleichheit+Extensionalität, Beta-Eta-Gleichheit und Betagleichheit+Axiomenschema tx=βt’x & x∉FV(t) ⇒ t=βt‘. Ohne Beweis.

Es gilt nun die η-Aufschiebung: (→βη)*=→β*→η*, das heißt, Anwendungen der Etareduktion kann man immer hinter die Betareduktion verschieben. Ohne Beweis.

Die Beta-Gleichheit und Beta-Reduktion dient der „Auswertung“ von Lambda-Ausdrücken. Der Ungetypte Lambda-Kalkül ist Turingmächtig. Hierzu definieren wir zunächst zwei Terme T=λx.λy.x, F=λx.λy.y, sie gelten als „Wahr“ und „Falsch“. Eine Anweisung der Form „if t then a else b“ kann man dann, wenn t∈{T,F}, ausdrücken durch tab.

Im Folgenden unterscheiden wir nicht immer sauber zwischen Beta-Gleichheit, Alpha-Gleichheit und Absoluter Gleichheit, da im Allgemeinen klar ist, was gemeint ist.

Paare (x, y) kann man codieren durch [(x,y)]=λs.s[x][y], wobei Eckige Klammern Codierung semantischer Entitäten bedetuen soll. Dann setzen wir car=λp.pT und cdr=λp.pF, diese geben jeweils das erste bzw. das zweite Element eines Paares aus.

Natürliche Zahlen codiert man am Besten durch Church-Ziffern. Setze [0]:=λf.I, wobei I=λx.x die Identische Funktion sei, und [n+1]:=λf.λx.f(([n]f)x), also allgemein [n]=λf.λx.fnx.

Addition add[n][m]=add[n+m] erhält man, wenn man add=λn.λm.λf.λx.[n]f([m]fx), die Nachfolgerfunktion succ[n]=[n+1] analog.

Test auf 0 durch die Funktion zerop, sodass gilt zerop[0]=T, zerop[n+1]=F mittels zerop=λn.n(λx.F)T

Die Vorgängerfunktion ist schwieriger zu erzielen. Ich habe jetzt keine Lust dazu, sie abzutippen. Man findet sie sicherlich in jedem Standardwerk.

Freilich benötigt man ebenfalls Rekursion. Diese kann man z.B. durch den Standard-Fixpunktkombinator erreichen. Setze Y(s):=(λx.s(xx))(λx.s(xx)), und Y:=λs.((λx.s(xx))(λx.s(xx))). Es gilt Ys=s(Ys). Also Rekursion. Wichtig ist hierbei: Rekursive Aufrufe haben immer einen nicht-terminierenden Zweig. Es kommt also auf die Auswertungsreihenfolge an. Das ist ein bekanntes Problem, das auch in funktionalen Programmiersprachen auftritt.

Mit diesem Wissen kann man nun relativ leicht (aber leider nicht besonders elegant) zeigen, dass Betareduktion Turingmächtig ist. Am dem Rand dieses Blogs ist leider nicht genug Platz, um den Beweis zu notieren.

Wenden wir uns stattdessen der Beobachtbaren Gleichheit zu, das heißt dem Versuch, Terme zu vergleichen, ohne deren genauen Inhalt zu kennen. Wir definieren die Relation # zwischen zwei Termen durch s#t :⇔“durch die Hinzunahme von s=t als Regel zur Beta-Gleichheit lässt sich T=F herleiten“. Sprich „s unbedingt ungleich t“.

Satz von Böhm: Sind v und v‘ zwei unterschiedliche βη-Normalformen, so gilt v#v‘. Ohne Beweis. (Ja, ich weiß, ohne Beweis ist es langweilig, aber mei…)

So… Jetzt käme ich eigentlich zum Getypten Lambda-Kalkül… Aber wenn ich ehrlich bin, habe ich jetzt keine Lust mehr! Gute Nacht!

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: