Frage zur Übung 6 Aufgabe 1 (MuLö)

Benutzeravatar
Dennis
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 102
Registriert: 29. Sep 2008 21:15

Frage zur Übung 6 Aufgabe 1 (MuLö)

Beitrag von Dennis »

Ich bin gerade etwas durcheinander.

Ich möchte die Herleitungen zeigen bei Aufgabe 1 Teil 2 - a

In dem Schritt der Teilherleitung, die mit Hw bezeichnet wird, wird die Regel rwht angewendet. Mir ist nich ganz klar, inwiefern ich dort die Zustände o'' und o' zu ersetzen habe (o soll in dem Fall das kleine sigma sein).

In den Folien für Com wird bei rwht auf der rechten Seite aus einem " o -> o " ein " o'' -> o' "
In der Musterlösung wird hier jedoch aus o'' -> o' ein o' -> o'.

Mir ist klar, dass wir schon irgendwie auf o' -> o' kommenn wollen, weil wir dann rwhf anwenden können bzw. keine Zustandsänderung eintritt.
Aber ich dachte, dass das Kalkül quasi vorgibt, dass ich aus dem aktuellen zustand (o ohne strich) dann oberhalb der Linie die vorherigen Zustände hinschreiben muss, also das aus z.B. o'' -> o' sowas wie o'''' -> o'' werden würde.

Offensichtlich werfe ich mit meiner Interpetation der kleinen Sigma etwas durcheinander, sodass sich mir gerade nicht erschließt, warum wir jetzt statt noch zwei Schritte zurück zu gehen wir quasi o'''' = o' haben.
...fragt stellvertretend für alle Freunde...

derDaniel
Mausschubser
Mausschubser
Beiträge: 76
Registriert: 2. Mai 2012 15:25

Re: Frage zur Übung 6 Aufgabe 1 (MuLö)

Beitrag von derDaniel »

Also ich verstehe von deinem Post nur Bahnhof :b

Vielleicht kann ich aber trotzdem helfen.
Man muss beachten, dass ja hier die Prämisse gilt, dass der if-Ausdruck herleitbar ist. Dadurch erhält man bereits bestimmte Auswertungen und Herleitung, die man sich im while-Ausdruck zu Nutze macht.

Das o' -> o' ausgewertet wird liegt doch daran, dass hier der guard in while zu false auswertet und deswegen der Zustand unverändert bleibt.

Antworten

Zurück zu „Archiv“