Verständnisproblem alternative Semantik Com

dees
Windoof-User
Windoof-User
Beiträge: 28
Registriert: 6. Mär 2011 14:01

Verständnisproblem alternative Semantik Com

Beitrag von 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)
Bild

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:
Bild

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
Erstie
Erstie
Beiträge: 19
Registriert: 26. Mai 2011 17:23

Re: Verständnisproblem alternative Semantik Com

Beitrag von 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)

Antworten

Zurück zu „Archiv“