Verständnisproblem alternative Semantik Com

[dees]

Hallo,

ich habe ein Verständnisproblem bzgl. der alternativen Semantik von Com aus Übung 8.2

z.B. sind mir folgende Sachen unklar:
1)


In der Beschreibung der Übung steht "dass ein Kommando c im Zustand sigma durch einen primitiven Berechnungsschritt zum Programm c' im Zustand simga' reduziert wird" und weiter "dass ein primitiver Berechnungsschritt genau einen Ausdruck aus Aexp, Bexp... auflösen kann.

Das müsste doch bedeuten, dass bei obigem Kalkül "b" ausgewertet wird und ich dann im Zustand sigma' bin also statt \(<c_1,\sigma>\) eigentlich \(<c_1,\sigma'>\)


2)
Des weiteren ist ist mir auch die Alternative zu dem Kalkül nicht ganz klar:


Warum wertet die Konklusion jetzt zu \(<c_1',\sigma'>\) aus? Ich habe doch nur einen einzigen primitiven Berechnungsschritt bei der Reduktion, welcher ja schon bei \(<b, sigma> => true\) verwendet wird, warum kann ich jetzt also noch einen zweiten Berechnungsschritt haben, indem \(<c_1,\sigma> \rightarrow <c_1',\sigma'>\) auswertet?

gruß

[r1chard]

zu 1)
das wäre richtig, allerdings wird bei der Auswertung von b (in Bexp) \(\sigma\) garnicht verändert.
also wäre dein \(\sigma' = \sigma\)

(\(\sigma\) beschreibt ja die Variabelnbelegung, die sich nur bei einer Zuweisung ändern, vgl. Übung 5 Aufgabe 1.2)

zu 2)
Hier wird eigentlich genau das gleiche gemacht, nur das ein weiterer Schritt gleichzeitig gemacht wird.

In der Prämisse kann man ja beliebig viele Vorbedigungen haben, also kann man auch schon einen weiteren Auswertungsschritt machen,
theoretisch könnte man auch so etwas schreiben wie:

\(rift''
\Large {
{<b,\ \sigma>\ \Rightarrow\ true \ \ \ \ <c_1,\ \sigma>\ \rightarrow_1\ <c_1',\ \sigma'> \ \ \ \ <c_1',\ \sigma'>\ \rightarrow_1\ <c_1'',\ \sigma''>}
\over
{<if \ b \ then \ c_1 \ else \ c_2\ fi,\ \sigma>\ \rightarrow_1\ <c_1'', \sigma''>}
}
\normalsize
c_1' \neq \epsilon\)

man müsste allerdings in den Bedingungen sicherstellen, dass man \(<c_1',\ \sigma'>\) noch einmal auswerten kann (ich hoffe, dass man das einfach so schreiben kann)

also:
Prämisse beliebig viele Urteile, Konklussion ein Urteil (vergleiche Modul 7 Folie 18)