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üß.
