1) Hintereinanderausführung:

Auf Seite 15 im Script steht:

[c_0;c_1]_comm sigma = [c_1]_comm([c_0]_comm sigma)

Das das ganze nicht gilt, ist mir bewußt, allerdings verstehe ich die Notation von [c1]_comm([c_0]_comm sigma) nicht so ganz. Das ganze sagt mir einfach nur, das [c_1]_comm mit dem Zustand der sich aus der Klammer ergibt ausgewertet werden würde, oder? Sprich, bei drei Anweisungen würde es (falsch) heißen:

[c_0;c_1;c_2]_comm sigma = [c_2]_comm([c_1]comm([c_0]comm sigma))

bzw. richtig dann:

([c_2]comm)_doppelbottom ([c_1]comm)_doppelbottom ([c_0]comm(sigma))


2) Bedeutung einer Formel aus <comm>

Warum die doppelte Abbildung: [-]_comm : <comm> -> SIGMA -> SIGMA_bottom? Also erst von <comm> zu SIGMA und dann noch von SIGMA zu SIGMA_bottom?

-> Hab's doch verstanden, glaube ich: Anweisungen sind der Übergang von einem Zustand zum nächsten.

jo

ok!

<comm> ist die Menge der Anweisungen, Programme, simple Syntax

jeder Anweisung wird eine Auswertungsfunktion zugeordnet, eine Funktion von SIGMA nach SIGMA_bottom

[-]_comm leistet diese Aufgabe,
[-]_comm ist selber eine Funktion die einem Programm eine Auswertungsfunktion zuordnet

also [-]_comm : <comm> -> (SIGMA -> SIGMA_bottom)

Ah!

3) Substitutionstheorem für Anweisungen
Mir sind gerade die Notationen "([c]_comm sigma)w" bzw. "[sigma|v:0]w" nicht klar. Was macht denn eine Variable hinter einem Zustand? Oder lese ich das gerade komplett falsch?

ein Zustand ist ja selber wieder eine Funktion ;)

sigma von w ist der Wert/ die Belegung der Variable w in diesem Zustand