Disclaimer: Dieser Thread wurde aus dem alten Forum importiert. Daher werden eventuell nicht alle Formatierungen richtig angezeigt. Der ursprüngliche Thread beginnt im zweiten Post dieses Threads.
Aufgabe 3.11
Teil 1, Bisimulation definieren - geschenkt, aber den zeiten Teil versteh ich nicht.
Was machen die beiden Listen, die ich det uebergeben muss? (insbesondere die zweite?) Irgendwie ist mir das alles nicht so klar…
det hat zwei Argumente:
(1) Eine Funktion a → List b, die das Verhalten des Bots beschreiben soll: Abh. von der Eingabe soll der Bot einige b’s (List b) ausgeben.
=> In der Eigenschaft (a) für mute ist die Funktion (\a → Nil), also egal welche Eingabe - keine Ausgabe.
(2) Eine Liste von b’s die der Bot noch ausgeben muss bevor er wieder auf Eingabe wartet.
=> In Eigenschaft (a) ist das Nil, da mute ja nichts ausgeben darf.
Muss man für die Beweise bei der 11.2 Koinduktion benutzen?
Wenn ja, wie kann man zeigen dass die Zustände gleich sind?
Selbstverständlich Koinduktion. Und wie man das macht wurde in der Vorlesung und Übung gezeigt: Bisimulation. Deswegen Teil (1), wo man das Bisimulations-Schema angeben soll.