Dieser Audiobeitrag wird von der Universität Erlangen-Nürnberg präsentiert.

Ich erinnere kurz daran, wo wir im Material sind.

Wir wollen letztlich los darauf zu etablieren, dass bestimmte Systeme,

die wir vor uns haben, eine gute Eigenschaft haben, die nennen wir die

Church-Rossa Eigenschaft oder eben Konfluenz.

Wir kennzeicheln am besten durch so diamantenförmige Diagramme, rautenförmige

Diagramme, auf Deutsch vielleicht besser. Die fangen an damit, dass ich annehme,

dass ich einen Term auf zwei Arten reduzieren kann und zwar jeweils hier bei

der Foyer & Schautrasser Eigenschaft in mehreren Schritten und verlangen dann,

dass sich das wieder zusammenführen lässt, diese auseinanderlaufende

Reduktion, ebenfalls eventuell in mehreren Schritten.

Und wir hatten eine schwächere Variante davon eingeführt, die sogenannte lokale

Konfluenz oder schwache Church-Rasser Eigenschaft, deswegen WCR wie Weak Church-Rasser.

Da sieht das Diagramm fast genauso aus, nur dass ich eben jetzt nur für solche Terme

Zusammenführbarkeit verlange, die ich bekomme, indem ich einen Ausgangsterm in

jeweils einem Schritt in zwei Richtungen reduziere.

Hier würde ich also auch wieder verlangen, dass ich diese beiden Eckpunkte

hier in eventuell mehreren Schritten unten zu einem Term wieder zusammenführen

lässt. Ein Beispiel, das wir am Ende gesehen hatten, wo das gut klappte, war

dieses hier. Das war aus unserem Beispielreduktionssystem aus der Theorie

der Gruppen. Wenn sich noch jemand fragen sollte, warum macht der Schröder so

komische mathematische Sachen, dann denken sie meinetwegen Transformation der Ebene

oder sowas oder des 3D-Raums, wenn sie gerne Computergrafik machen oder sowas.

Mit diesen Matrizen, die sie da anwenden, haben sie dann eine Gruppe vor sich.

Also es ist auch etwas, was durchaus sehr anwendungsorientierte Leute interessiert.

Also hier Theorie der Gruppen, das würde uns also hier zwei Dinge erlauben.

Erstens dürften wir diesen Ausdruck hier umklammern, nach links, oder wir dürften

hier das neutrale Element streichen. Da hätten wir also zwei verschiedene

Reduktionen und wir können uns fragen, ob die wieder zusammenführbar sind und wir

haben gesehen, dass sind sie. Nämlich zum Term x mal y.

Wir verlangen ja nur, dass es in beliebig vielen inklusive Null Schritten

geht. Nun zufällig ist es hier gerade mal einer und hier keiner.

Wir sehen auch noch andere Beispiele jetzt nachher, wo es irgendwie auch mal

mehrere Schritte sind, die man braucht. Wir verallgemeinern jetzt eben noch

mal diese Situation hier und verschaffen uns dann ein bisschen Notation.

Also wir unterstellen jetzt einen Term s, den wollen wir reduzieren.

Ja, wie reduzieren wir nun? Wir spalten den Term auf in einen Kontext. In dem

Kontext steckt die linke Seite einer Umformungsregel und unter dieser linken

Seite hängt wieder eine Substitution. Das ist ja die Art, wie diese

Einschrittreduktion funktioniert.

Das s könnte von der Form sein C1 von L1 sigma 1, wobei sigma 1 eine

Substitution ist, L1 die linke Seite einer Grundreduktion und C1

irgendein Kontext, in dem das steckt. Und wenn wir dann Pech haben, geht das auch

noch auf eine andere Art. Also ist man nur mit Index 2 dran statt 1. Also wiederum

in einem Kontext habe ich die linke Seite einer Reduktionsregel und darunter habe

ich eine Substitution. So gut, das heißt, hiernach könnte ich das jetzt jeweils

reduzieren. Da kommt dann raus

jeweils die rechte Seite der Grundreduktion. Also hier sagen wir R,

nicht 2, natürlich R1. Immer noch im selben Kontext und mit der selben

Substitution drunter und hier rechts genauso. Da haben wir also C2 von R2 sigma 2.