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

Ja, herzlich willkommen.

Übliche Frage vorweg, braucht noch jemand eine Tanne?

Nein, nur bekannte Gesichter im Saal.

Ja, gut.

Sind Sie letzte Woche mit Herrn Hausmann klargekommen?

Gibt es Fragen zu letzter Woche?

Da macht er das ja besser als ich bestens.

Okay, um jetzt den dritten Zettel bearbeiten zu können, braucht man noch ein Detail zum

Thema mehrsortige Datentypen, was ja letztes Mal das Thema war, oder sagen wir mal noch

ein Beispiel zum Thema mehrsortige Datentypen.

Die Definitionen sind an sich alle da.

Das letzte Beispiel dafür ist nicht mehr gereicht, machen wir das also eben.

Und zwar zum Thema, gegeben eine mehrsortige Datentyp, Definition oder Deklaration, wie

extrahiere ich daraus einen B-Simulationsbegriff, mit dem ich die Gleichheit von Programmen zeigen

kann?

Das geht wie folgt.

Machen wir mal eine mehrsortige Definition.

Also, ne, halt, Korrektur, der Punkt ist nicht so sehr, wie es in der Mehrsortigkeit geht,

sondern wie es dann funktioniert, wenn man Input hat.

Also, wenn man einen Nachfolger hat, der von außen kommenden Input abhängt.

So und zwar wird das ein Datentyp, der ist sehr ähnlich wie dieser Terrain-Datentyp,

den Sie letztes Mal gesehen haben.

Inf, wie, infinite oder sowas, also mit unendlich vielen Richtungen.

Und dazu geben wir dem Typ zwei Parameter mit.

Einmal das übliche A, was also das bezeichnet, was wir so an Einträgen lokal vorfinden,

also die örtlichen Features gewissermaßen.

Und ein Typ D von Richtungen, also D wie Direction.

So und wenn wir da also so durchlaufen, durch das Terra, dann haben wir einmal diesen Beobachter

Objects.

Ah, jetzt habe ich es ja andersrum als im Skript, das sollte ich nicht machen.

Also die Reihenfolge der Parameter ist da, nicht ad.

So, der geht von Inf Terrain oder Terrain, oder wie auch immer wir das aussprechen wollen,

da nach List a.

Der sagt uns also, was finde ich also hier gerade für Objekte vor.

Ja, das ist wie so ein alten Infocom Adventure, there is an axe here oder auch mehr.

Und dann kann ich mich außerdem noch bewegen.

Und ich kann mich bewegen, nicht nur einfach so, sondern ich kann mich in eine bestimmte

Richtung bewegen und der Typ der Richtung ist eben gerade das D.

Das heißt, ich habe hier ein weiteres Argument vom Typ D.

Und was rauskommt ist wieder vom Typ Inf Terrain da mit anderen Worten, ich habe mich irgendwo

anders hin bewegt, von wo ich mich dann wieder woanders hin bewegen kann und wo dann auch

wiederum eventuell andere Objekte herumliegen.

So, das ist unser Datentyp, da lesen wir jetzt zunächst mal ab die Struktur des Mengenoperators,

für das dieser Datentyp, die Finale oder dieser Codatentyp, die Finale Co-Algebra sein soll.

Also wie steht es definiert so ein Datentyp die Finale Co-Algebra für einen Mengenoperator

und zwar hier den Operator, der eine Menge x abbildet auf ein Kreuzprodukt und zwar

nicht, also deswegen ein Kreuzprodukt, weil ich hier zwei Beobachter habe.

Und gut, der erste Beobachter, der gibt mir also eine Liste über a, ich schreibe wieder

salopp einfach A für die Interpretation von kleinen a, das ist also hier das Ergebnis