Not logged in. · Lost password · Register

momo8
Member since May 2015
69 posts
Subject: 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.


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 }
1) hd(unfold fst flip (0,1) )= fst(0,1)= 0
    hd(alt 01) =0   passt!
2) 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}

1) hd(unfold fst flip (1,0)) = fst(1,0) = 1
  hd(alt 1 0)=1 passt
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




Marcel[Inf]
#faui2k15, GTI-Tutor a. D.
Member since Nov 2015
620 posts
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?
momo8
Member since May 2015
69 posts
https://prnt.sc/mlee1c ist mir sihcer, die Aufgabestellung stimmt
momo8
Member since May 2015
69 posts
In reply to post #2
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)
Marcel[Inf]
#faui2k15, GTI-Tutor a. D.
Member since Nov 2015
620 posts
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.

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
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.
Close Smaller – Larger + Reply to this post:
Verification code: VeriCode Please enter the word from the image into the text field below. (Type the letters only, lower case is okay.)
Smileys: :-) ;-) :-D :-p :blush: :cool: :rolleyes: :huh: :-/ <_< :-( :'( :#: :scared: 8-( :nuts: :-O
Special characters:
Go to forum
Datenschutz | Kontakt
Powered by the Unclassified NewsBoard software, 20150713-dev, © 2003-2011 by Yves Goergen