Ja, herzlich willkommen!

Vorweg die Tech-FackThay erinnert nochmal an die Evaluation.

Es gibt bisher 17 Rückläufer,

das also ungefähr die Hälfte oder etwas weniger der im Saal anwesenden Personen ist.

Ich ermutige also nochmals zur Teilnahme.

Wer noch keine TAN hat, möge sich melden, aber ich glaube.

Sieht sich.

Ja, wir fahren fort beim Thema Ko-Rekursion und Ko-Induktion über Datentypen mit Alternativen,

nennen wir das jetzt.

Ich erinnere nochmal an unseren Datentyp Endlicher oder Unendlicher Listen bzw. unseren Ko-Datentyp,

der aus folgenden Destruktoren besteht.

Ein Destruktorenend, der in dem Falle definiert ist, dass halt die Liste schon zu Ende ist,

das ist also der Destruktor der leeren Liste, der liefert nichts zurück, ist halt dann in

dem Falle einfach nur definiert, das ist die einzige Botschaft, die er mit sich bringt.

Und dann gibt es weiterhin eine Head-Funktion, die aber nur dann definiert ist, wenn die

Liste eben nicht leer ist, sondern noch weiter geht.

Der ist dann definiert auf dieser zweiten Alternative, die nennen wir Alive, also ist

mir so eine Sicht auf Listen eben als Streams, die also entweder noch weiter gehen können

oder irgendwann kaputt sein, geht nach A, also liefert wie üblich den Kopf und entsprechend

geht Tail von derselben Alternative nach Liste A.

So wir hatten uns formal überlegt, wie ein Begriff von Signatur aussieht, der solche

Dinge einfängt, das ist dann also ein Begriff von Signatur, der herkommt, zerlegt in eine

große desjungte Summe, eine praktisch für jede Alternative, also hier haben wir zum

Beispiel letztlich diese Mengenkonstruktion hier, die also eine Menge x abbildet auf 1

plus, also das ist die erste Alternative hier, dead, plus a Kreuz x, wie der Mengenkonstruktor

für Streams, das hier ist eben die zweite Alternative Alive, das hier ist dead.

So, ja wir hatten uns überlegt, wie erstens wie gesagt diese Q-Signaturen aussehen, die

also dann pro Alternative genau eine Kopffunktion haben und je nach Stelligkeit, also je nach

dem was wir hier oben noch für einen Exponenten dran schreiben, eine Anzahl von Tailfunktionen,

sodass also wahlweise, wenn es genau einstellig ist, wie hier immer so eine lineare Fortentwicklung

da ist oder wenn es mehrstellig ist, halt eine verzweigende Fortentwicklung des Prozesses.

Und wir hatten uns außerdem überlegt, wie sich Co-Algebren für diese Mengenkonstruktion

hier, die wir ja vorher schon definiert hatten, also Abbildungen von irgendeinem n in g von

n, wie die sich in Begriffen solcher Co-Signaturen darstellen.

So, es ist noch ein bisschen was übrig.

Wenn jetzt Sigma so eine Co-Signatur ist, ja dann schreiben wir ja so den durch Sigma

oder ja durch die Co-Signatur Sigma definierten Co-Datentyp, wie auch schon im Falle der Algebren.

So, und im Falle der Algebren war das die initiale Sigma-Algebra, entsprechend ist das hier die

finale g Sigma Co-Algebra, wo ja bei eben g Sigma sich in der diskutierten Weise aus

dieser Co-Signatur ergibt.

So, die wollen wir ja halbwegs formal beschreiben, nicht endlos formal.

Also, was sind die Zustände, darauf werde ich mich jetzt mal beschränken, zu beschreiben,

was hier also die Zustände in dieser finalen g Sigma Co-Algebra sind.

So, die Zustände in dieser finalen g Sigma Co-Algebra, die sind Bäume.

Die können endlich sein, wenn nicht so wie hier im Falle der endlichen oder inendlichen

Listen, also so eine Liste kann auch mal abbrechen, dürfen aber auch unendlich sein und alle

Bäume der jetzt gleich genauer beschriebenen Art, ob endlich oder unendlich, kommen halt

als Zustände in der finalen g Sigma Co-Algebra vor.

Die Knoten dieser Bäume sind beschriftet mit zwei Dingen.

Erstens, erstens sind sie beschriftet mit einer Alternative,