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.
SS2018 Klausur Aufgabe4 Frage an Koinduktion Kann jemand sehen, was ich falsch gemacht habe?
Aufgabe 4 Korrektion und Koinduktion
2. Folgende Aufgaben verwendet wir Paartypen(a,b) .
gegebende Funktion:
flip(x,y)=(y,x)
fst(x,y)=x
hd(unfold h t x)= h x
tl(unfold h t x)=unfold h t ( t x)
hd(alt x y) = x
tl(alt x y ) = alt y x
Beweisen Sie folgende Eigenschaft durch Koinduktion: unfold fst flip (0,1) = alt 0 1
wobei wir 0 für Zero und 1 für Succ Zero schreiben . Rechtfertigen Sie alle Beweisschritte.
[b]die Aufgabe ist eigentlich einfach, aber …
Meine Lösungsweg ,
(Diese Aufgabe soll einfach Bisimulation beweisen)
R= {(unfold fst flip (0,1) ,alt 0 1)l }
-
hd(unfold fst flip (0,1) )= fst(0,1)= 0
hd(alt 01) =0 passt! -
tl(unfold fst flip (0,1) ) = unfold fst flip (flip (0,1) =unfold fst flip (1,0)
tl (alt 0 1) = alt 10
tl sind nicht gleich, dafür muss ich R erweiter
R`= R U{(unfold fst flip (0,1) ,alt 10),l} -
hd(unfold fst flip (1,0)) = fst(1,0) = 1
hd(alt 1 0)=1 passt -
tl(unfold fst flip (1,0)) = unfold fst flip (0,1)
tl (alt 1 0 ) = alt 01
dann ich komme nicht weiter, kann jemand helfen!!! Bitte
[/b]
Bist du sicher, dass die Aufgabenstellung korrekt ist?
So wie ich das sehe, sind x und y überall Streams.
(Selbstnotiz bzw. an die, die mehr als ThProg wissen: D.h. wenn diese Streams über den Typ O sind, dann arbeiten wir mit dem Funktor FX := OxX und mit der Koalgebra O^\omega x O^\omega → O x (O^\omega x O^\omega) via <hd \circ fst, <tl \circ snd, tl \circ fst>>.)
Das macht aber immer noch keinen Sinn, weil (0, 1) kein Stream ist. Wie soll unfold darauf aufgerufen werden?
ich habe jetzt die Viedoaufzeinung 17 angeschaut, ich soll einfach CO-IV einzusetzen, dann passt einfach meine Beweisen. (Unter der Viedoaufzeichnung 17 Beispiel odd(b 0 s)= s den Fall)
Ah, mein Fehler! Für Typen A, B betrachtet man den Paartyp (A, B). Die betrachtete Koalgebra ist B → A x B (damit der Funktor FX := A x X) und unfold bekommt eben diese Koalgebrastruktur als (B → A) und (B → B) und liefert den eindeutigen Morphismus B → Stream A.
[quote]2) tl(unfold fst flip (1,0)) = unfold fst flip (0,1)
tl (alt 1 0 ) = alt 01
dann ich komme nicht weiter, kann jemand helfen!!! Bitte[/quote]
Dein R’ ist ein bisschen falsch, siehe mein R unten. Du solltest (alt 1 0) statt (alt 0 1) schreiben. Der letzte Schritt wäre zu sagen: unfold fst flip (0, 1) R’ alt 0 1.
Wenn du so willst, ist das eine Koinduktions-IV. Der vollständige Lösungsweg wäre:
Def. R = {(unfold fst flip (0,1), alt 0 1), (unfold fst flip (1, 0) ,alt 1 0)}. Sei u R v. Zz. ist, dass (hd u = hd v) und (tl u R’ tl v).
Fall 1 (linkes Tupel):
- hd (unfold fst flip (0,1)) = fst (0, 1) = 0 = hd (alt 0 1).
- tl (unfold fst flip (0,1)) = unfold fst flip (flip (0, 1)) = unfold fst flip (1, 0) R (alt 1 0) = tl (alt 0 1)
Fall 2 (rechtes Tupel): analog.