Ich denke bei „applikativer Auswertungsreihenfolge“ gehen Vorlesung und Übung auseinander, „leftmost innermost“ kam in der Vorlesung afaik nicht dran, wäre aber wohl die übliche Java-Variante.
In der Vorlesung hatten wir:
ts →a ts’ (wenn s →a s’)
ts →a t’s (wenn s normal)
was bei ((a b) (c)) wohl eher ein „rightmost innermost“ wäre.
Konkret nach Vorlesung:
„one“ ist nicht normal bzgl δ-Red, also zuerst das als „s“ auflösen. Der ganze Kram links davon ist ein großes „t“.
@ Hasenichts: Das stimmt. Also doch 4 statt 4’.
Stimmt, ich erinnere mich.
Damit wäre allerdings meine und Hasenichts’ zuvor gemachte Annahme, dass die Reihenfolge der Ersetzungen/δ-Reduktionen bei (a ( b c ) d) die „c, b, d, a“ ist, falsch.
Es wäre nämlich:
a ( b c ) d = ( a ( b c ) ) d
mit t = a ( b c ) und s = d
=> Vorlesungsregel (1), d wird ersetzt.
( a ( b c ) ) d
mit t = a ( b c ) und s = d (welches nun normal ist)
=> Vorlesungsregel (2), t wird bearbeitet.
usw.
Damit wäre ich bei der Reihenfolge d, c, b, a - falls b eine 1-stellige Funktion ist und bei d, c, a, b - falls b eine >1-stellige Funktion ist.
Diese Unterscheidung existiert wegen:
PS: Windfischs b) wäre dann auch in Schritt 3 schon wieder falsch.
Hat jemand einen Lösungsvorschlag zur Aufgabe 4?
Hier wäre meiner für die 4.1
sampler ( flat x ) s =
if (x == 0) then flat 0
else s
sampler t ( flat 0 ) = flat 0
sampler square( a b ) flat c =
if (a == 0 && b == 0) then flat 0
elseif (a == 0) then square( 0 c )
elseif (b == 0) then square( c 0 )
else flat c
sampler square( a b ) square( c d ) =
if (a == 0 && b == 0) then flat 0
elseif ( (a == 0 && d == 0) || (b == 0 && c == 0) ) then flat 0
elseif (a == 0) then square( 0 d )
elseif (b == 0) then square( c 0 )
else square( c d )
du definierst hier nur 2 Spezialfaelle des Samplers; wenn ich jetzt ein weiteres Signal, meinetwegen “Sägezahn” hätte, dann weiss ich nicht, wie sampler (Sägezahn 1 2) (flat 1) sich verhält.
hier mal meine 4, so wie ich glaube dass es stimmen müsste: http://ente.hawo.stw.uni-erlangen.de/~ki08jofa/thprog-A4.jpg
edit: meint ihr, das ist ausführlich genug? oder schon zu ausführlich?
Okay, das stimmt.
Nein, weil: currentSample : Signal → Int
Außerdem sind flat und square vom Typ Int → Signal bzw. Int → Int → Signal.
Ich bin bei der 4.1 auf das gleiche gekommen.
Die Lösung für Gleichung (2) sieht ziemlich ähnlich wie die von Gleichung (1) aus: Die Argumente der Vorkommen von „square“ werden wieder vertauscht und man muss R erweitern. Danach landet man wieder im ursprünglichen R.
Also nach dem ganzen Argumentationschaos habe ich meiner Meinung nach eine 2.1b), die stimmen müsste.
http://i.imgur.com/aA1ZqBJ.png
Dass man da erst one und dann two einsetzt müsste ja klammerungsmässig richtig sein, siehe a(bc)d=(a(bc))d von ceptoplex.
Um (2) zu zeigen, hättest du currentSample(sampler…) = currentSample(square x 0) und discardSample (sampler …) R discardSample (square x 0) zeigen müssen.
Du hast aber anstatt „square x 0“ immer „flat 0“ auf der rechten Seite verwendet.
Ich bin auf folgende Relation gekommen: R = {(sampler (square 1 0) (square 0 x), flat 0), (sampler (sqare 0 1) (flat x), square 0 x)}
Ich denke eher, dass das das Minimum an Ausführlichkeit ist. In der Klausur würde ich bei jedem Umformungsschritt noch angeben mit welcher
Gleichung ich das gemacht habe. Gibt ja doch recht viele Punkte auf die Teilaufgabe.
Er zeigt da nur die (1). In (1) muss man R um (sa(sq 1 0)(sq 0 x), flat 0) erweitern, damit R eine Bisimulation ist (ansonsten wäre nämlich ∀s,t ∈ R (discard s)R(discard t) nicht erfüllt).
Bei der (2) komme ich auf R = { (sa(sq 1 0)(flat x) , sq x 0) , (sa(sq 0 1)(flat x) , sq 0 x) }
Das rote kann man aus der Aufgabenstellung ablesen und das blaue ist wieder Resultat aus der Bedingung ∀s,t ∈ R (discard s)R(discard t) für Signal-Bisimulationen.
Ah 
. Die 2. Umformung von currentSample kann man sich aber sparen, da kommt R ja nicht vor.
Also braucht man für jedes Element von R eine erfolgreiche Umformung der Funktionen, die auf den koinduktiven Datentyp abbilden. Richtig?
Was meinst du damit?
So könnte man das vermutlich formulieren. Es geht einfach darum zu zeigen, dass alle „Paare“ in R auch wirklich aus zwei „gleichen“ Teilen bestehen.
Hat keinen Sinn gemacht, sorry.
Ich dachte, dass man bei currentSample die Gleichheit von linker und rechter Seite aus (1) reicht.
Aber man muss ja für alle s R t, currentSample s = currentSample t zu zeigen.
Ich bin mir bei Aufgabe 4 unsicher, weil wir hier ja nicht allgemein beweisen sondern konkret für diese Valuationen.
Mein Ergebnis sieht so aus wie bei Windfisch.
Aber darf ich wirklich einfach die Relation dann um eine konkrete Valuation erweitern ? Allgemein habe ich noch nicht verstanden was für diese Relation zulässig ist und was nicht.
Im Moment folge ich dafür dem Prinzip, dass ich schlichtweg aus dem zu beweisenden Satz abschreibe und bei Bedarf erweitere. Geht das methodischer ?
Du musst es dir so vorstellen: Eine Bisimulation enthält Paare, bei denen beide Teile äquivalent sind (deswegen muss R auch entsprechende Bedingungen erfüllen, damit es auch wirklich eine Bisimulation ist). Wenn du nun zeigen willst, dass zwei Signale s und t gleich sind, „erfindest“ du ein R, in dem das Paar (s,t) enthalten ist, und zeigst dann, dass R eine Bisimulation ist. Wenn nun R eine Bisimulation ist und (s,t) enthält, gilt folglich s=t.
Wenn nun R „erweitert“ wird, kannst du dir das einfach so vorstellen, dass man ein neues R versucht, weil das vorherige keine Bisimulation war. Das macht aber nichts. Wenn dieses neue R eine Bisimulation ist und (s,t) enthält, kann man daraus natürlich immer noch s=t folgern. Ganz oben das „richtige“ R hinzuschreiben (anstatt immer neue einzuführen) wie bei Windfisch macht das ganze natürlich wesentlich eleganter.
Ich denke der zweite Schritt ist das Einsetzen von pow2 (delta-Reduktion) und demnach erst der dritte Schritt die beta-Reduktion durch Einsetzen von \f a . f ( … ) in den Lambda-Term, mit dem man pow2 ersetzt hat. Ansonsten komme ich auf das gleiche Ergebnis wie du.
Meinst du, du schreibst pow2 erst als Lambda-Term hin? Weil sowas ist ja in der Aufgabenstellung nicht gegeben, da ist bloss die Funktion pow2 n = n (mult two) one
Gemeint ist wohl das hier (formal ausgedrückt - ich denke du meinst dasselbe) als einen Schritt auszudrücken:
pow2 λfa.f(f(fa)) →δ(β) (λfa.f(f(fa))) (mult two) one
… anstatt es als zwei Schritte zu betrachten:
pow2 λfa.f(f(fa)) →δ (λn.n (mult two) one) (λfa.f(f(fa))) →β (λfa.f(f(fa))) (mult two) one
Meiner Meinung nach ist aber in diesem Fall, bei dem in der Angabe schon eine β-Reduktion in eine δ-Schritt-Ersetzungsregel reinkombiniert wurde, das Ganze zusammen nur als ein Schritt zu werten (nämlich als δ-Reduktion).
(Also so wie ursprünglich als richtige Lösung angegeben.)
Meine Begründung: Wenn sie das nicht möchten, hätten sie ja die Angabe entsprechend anders formulieren können.
Womit wir übrigens auch wieder bei dem Thema wären:
[quote=ceptoplex:1411857292]Das mit der Schrittzahl würde mich auch interessieren.
Für mich heißt 4 Beta-Delta-Reduktionsschritte auch (wie in Windfischs Lösung), dass auch Nur-Delta-Schritte da dazuzählen - und nicht nur Schritte, in denen eine Beta-Reduktion stattfindet. Ist aber auch nur meine Meinung.[/quote]
Genau das meinte ich.
Hm ich les nicht aus der Aufgabenstellung heraus, dass das in einem Schritt gemacht werden soll. Egal, man kann ja sicherheitshalber fünf Schritte hinschreiben…
nach welcher Vorschrift hast du denn da entschieden, erst ‘one’ zu reduzieren? ‘two’ ist doch “mehr” leftmost UND innermost 
