Lambda-Kalkül, die Zweite

So. Im Moment bin ich in der Bahn. Mal sehen, was ich so alles zusammenbringe…

Aaalso… Wir sind bei der Standardreduktion stehengeblieben… Naja, was soll man dazu noch groß schreiben?

Gehen wir also Über zur Normalisierung… Ein Term t  heißt schwach normalisierend bezüglich einer Relation R, geschrieben t∈wn(R), wenn es einen Term v gibt, sodass tR*v, und vRw für kein w gilt. Er heißt stark normalisierend, und liegt in sn(R), wenn jede Reduktionsfolge terminiert.

η-Reduktion →η ist die kompatible Hülle von

⊢ λx.tx→ηt

βη-Reduktion ist die Relation die man erhält, wenn man  mehrere Betareduktionsschritte und anschließend mehrere Etareduktionsschritte erlaubt.

Etagleichheit und Beta-Eta-Gleichheit sind dann trivialerweise die kleinsten Äquivalenzrelationen darüber (also reflexiv-transitiv-symmetrische hüllen…)

Sei M eine Menge mit einer Verknüpfung, sodass mit r,s ∈ M auch stets rs∈M. Eine Relation R auf M heißt extensional genau dann, wenn gilt

rRr‘ ⇔ rsRr’s für alle s∈M

So… In meinem Skript ginge es jetzt mit dem Satz von Curry weiter, aber meine Internetverbindung wird gleich getrennt… Drum hör ich jetzt mal auf, solange, bis ich ankomme, ist ja nicht mehr so lange… Tschüß.

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: