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

Bevor wir in das Video beginnen, möchte ich etwas hinweisen, das ich am Montag nicht fertig sein konnte.

Das könnte euch mit dem Übungsgerät helfen.

Letztes Mal haben wir mit einem Konduktivtyp gespielt, das auf ein dynamisches Terrain gepräsentiert hat.

In dem wir an jedem Ort aufnehmen konnten, wo wir nach rechts oder links und absteigen konnten.

Das ist sehr einfach. Man kann sich ein anderes Terrain vorstellen, in dem man mehr als zwei Optionen hat.

Man hat 72 Optionen an jedem Schritt. Wir wollen nicht 72 verschiedene Observer haben.

Die Richtung 1, die Richtung 2, die Richtung 3, das wäre ein bisschen dumm.

Was man anstattdessen gerne machen möchte, ist, nur einen Observer zu haben, der eine Funktion ist, die,

was wir nehmen wollen, auf der nächsten Schraube führt.

Wir nehmen jetzt die Möglichkeit, absteigen zu bekommen, da das uns nichts mehr bringen kann.

Man könnte einen Typen definieren, den wir InfTerrain nennen, für Infinite Terrain.

Wir können nicht absteigen, so etwas.

Diesmal mache ich es parametrisch, nicht nur die Art von Objekten, die wir an jedem Schraubendruck finden,

sondern auch die Direktionen, die wir nehmen können.

Dies könnte ein Typen sein, das Vor- und Rück- und links- und rechts- und nord-eester- und nordwest-Vorwärts-Vorwärts-Vorwärts-Vorwärts hat.

Und dann würden die Observer, wie letztes Mal, etwas von einem Terrain geben,

das uns eine Liste von Objekten gibt, die wir auf der aktuellen Schraube sehen.

Dann würden wir nur einen Observer nennen, den wir dann,

wenn wir einen Infinite Terrain geben,

eine Funktion geben, die uns, wenn wir eine Direktion nehmen, auf die nächste Schraube sendet.

Die Paranthesis, die wir an der Konvention benutzen, sind nicht nötig, ich nehme sie nur als Einfluss.

Wir können diese Konduktivtype als eine Koalgebra für einen Funktor T, D-Rov, A,

in diesem Fall, in dieser Art, uns in Liste von A plus,

und nun die Notation, die man typisch für eine Funktion benutzt, ist so,

das sollte so gelöst werden wie, ja, ja, klar, wo sind sie?

Hier schon.

So, das ist ein Times und das ist eine Funktion von Direktionen zu x.

Also, letztes Mal, stattdessen, haben wir es so geschrieben,

was als ein Paar von x sein könnte, aber wir können es auch als eine Funktion von einem Set mit nur zwei Elementen zu x sehen,

was ein isomorphisches Objekt ist, das ist eigentlich das gleiche.

Und wenn wir uns die letzte Koalgebra für diese ansehen, dann ist es ein Baum von infiniter Höhe,

und die Bremsung des Baums ist von der Kardinale von dem, was wir hier auspicken.

Also, wenn wir sieben Direktionen haben, dann haben wir Tres mit sieben Abfällen auf jeder Note.

Und jetzt die Frage, was ist das Bissimulation Notion für diese Art von Dingen?

Es sollte nicht schwer sein, zu sehen.

Wir sagen, dass R ein Info-Terrain ist,

durch Bissimulation.

Also, jetzt haben wir zwei Elemente und wollen sehen, ob wir sie ein Teil erzählen können,

oder ob wir sie in irgendeinem Fall bezeichnen können. Also, welche Tests, was sollten wir machen können?

Wir sollten zuerst die Objekte in der aktuellen Position vergleichen.

Das ist wie die letzte Zeit.

Die erste Beziehung, die wir letzte Zeit verwendet haben, war, dass wir die Elemente nicht bezeichnen konnten,

indem wir links und rechts auf beiden Sachen gehen.

Aber jetzt ist die gleiche Beziehung, dass wir die Elemente nicht bezeichnen können,

indem sie in der gleichen Richtung auf beiden Abfällen gehen.

Die zweite Beziehung ist, dass für alle Direktion D,

wenn wir an x auf Direktion D gehen,

wir nicht bezeichnen können, was wir da bekommen, was wir sehen, wenn wir in der gleichen Richtung auf y gehen.

Und wieder zeigt man, dass, wenn zwei Dinge, wenn es eine Bissimulation zwischen zwei