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

Ja, wir haben noch zwei Sitzungen vor uns. Die eine Sitzung heute wollte ich verwenden

eben auf ein weiteres Eingehen über koinduktive Vorgehensweisen in der Theorie regulärer Sprachen.

Und am Donnerstag kommt dann das Piesteresistens, der starke Normalisierungsbeweis für Lambda 2.

Ja,

ich erinnere nochmal an das Ende der letzten Sitzung.

Da hatten wir uns nochmal Gedanken gemacht, was ist denn ein Morphismus von Transitionssystemen,

wenn wir uns darauf einlassen, dass wie eingesehen Transitionssysteme Koalgebren für eine bestimmte

Mengenoperation sind und wir einfach den Begriff von Koalgebrenorphismus, den wir daraus bekommen,

uns übersetzen. Und das sah so aus. Zum einen sollte so ein Morphismus verträglich sein mit

Finalität von Zuständen. Das heißt, er soll eben finale Zustände auf finale abbilden und auch nur

solche. Das heißt also auch nicht Finale auf nicht Finale. Und

ich bleibe jetzt mal bei unserer Koalgebraschennotation, wo wir also hier die Argumente

vertauschen, Currying verwenden, also eine Funktion zunächst auf einen Zustand anwenden und dann eine

Funktion bekommen, die noch einen Buchstaben aus dem Alphabet erwartet. Können wir also sagen,

gut zum einen wenden wir erst unseren Morphismus an und dann im Zielbereich, ich bezeichne die

jetzt mal alle nur mit B und A, nicht B0, A0 und so weiter, im Zielbereich unsere Transitionsfunktion

darauf anwenden oder wir können erst auf der linken Seite schon die Transitionsfunktion

anwenden und dann mit F nach B rübergehen und das soll jeweils denselben Zustand ergeben.

Und wir hatten uns ja vorher überlegt, dass das finale Transitionssystem eben gerade die

Menge Großländer der Sprachen ist mit einer Struktur, die gerade eine Sprache als final

erklärt, wenn sie das leere Wort enthält und deren Transitionsstruktur gerade durch

diese Sprachableitung gegeben war. Und diesen eindeutigen Morphismus, den hatten wir wie

folgt beschrieben. Jetzt habe ich hier einmal Zustände X und einmal Q genannt, man folge

mir da. So und da wird eben so ein Zustand in einem Transitionssystem, der ja aus dem

Transitionssystem, wenn man ihn dann auswählt als initialen Zustand einen Automaten macht,

der wird abgebildet auf die von diesem Automaten akzeptierte Sprache. So, nicht das war das

letzte Resultat, das wir in der letzten Sitzung gesehen haben. Ja, das Corollar dazu, was ich

jetzt noch anschreiben möchte, das wendet diese Einsicht an auf etwas, was wir uns mal

im Zusammenhang mit Streams überlegt hatten oder dem Stichwort Verhalten. Wir hatten definiert

ja das Verhalten eines Zustands in einer Co-Algebra als sein Bild in der finalen Co-Algebra.

So, hier steht, das Bild eines Zustands in der finalen Co-Algebra ist die von ihm akzeptierte

Sprache. So, nicht das heißt also Sprache gleich Verhalten für solche Co-Algebren für

diesen, ich habe eben doch Funktor gesagt, Nängenoperator. Und wir hatten uns das Verhalten

zwei ganz elementare Sachen überlegt, die sich jetzt hier instanzieren auf Sprachen.

Wenn ich mir das finale Transitionssystem Lambda angucke, dann sind die Zustände im finalen

Transitionssystem ja gerade die Sprache. So, ich kann also dieses Prinzip hier, kann ich

insbesondere auf A0 gleich Lambda loslassen. Und wir wissen ja, weil es nur einen Morphismus

gibt, ist dieser Morphismus die Identität. So, das heißt, als Zustand im finalen Transitionssystem

akzeptiert L gerade die Sprache L. Ja, das hatten wir allgemeiner hingeschrieben über

das Verhalten eines Zustands in der finalen Co-Algebra ist er selbst. Und zweitens, Morphismen,

Ergänze von Transitionssystemen natürlich. Morphismen bewahren akzeptierte Sprachen,

das haben wir uns auch allgemein über Verhalten überlegt. Ein Morphismus von Co-Algebren,

der bewahrt das Verhalten, das liegt einfach daran, nicht einfach weiterhin an der Eindeutigkeit

des Morphismus in die finale Co-Algebra, hatten wir uns überlegt. So, hier heißt also Verhalten

gleich Sprache, das heißt, Morphismen bewahren akzeptierte Sprachen, das heißt, einmal ausgeschrieben.

Wenn ich so einen Morphismus habe, f, dann ist die im Zielbereich, also f wieder oben,

dann ist die im Zielbereich f0 vom Zustand fq akzeptierte Sprache dieselbe wie die im

Ausgangsbereich a0 von q akzeptierte Sprache.

So, damit können wir jetzt lossteuern auf eine Co-Algebraische Abhandlung ernsthafter