S[['while' E 'do' L 'od']](Env) = cond(E[[E]](Env);L[[L]](Env) o S[['while' E 'do' L 'od']](Env);id(Env))
Hierbei ist id die Identity Function, für die gilt :
id(Env) = (Env)
Diese muß hier angewandt werden, da Bedingungen mit nur einem Zweig nicht definiert wurden.
Diese Definition zeigt auf, daß die semantik der While Schleife ein Fixpunkt der Funktion F ist.
F(g) = cond(E[[E]];g o S[[S]];id)
Es muß gewährleistet sein, daß F genau einen Fixpunkt besitzt. Die Beweisführung, daß
ein keinster eindeutiger Fixpunkt für eine Funktion F existiert, ist essentieller Bestandteil
der Domaintheory. Hier soll angenommen werden, daß die einzige zu beachtende Komplikation der Fall
einer nicht terminierenden Schleife ist. Für diesen Fall soll in Anlehnung an das bekannte Verhalten
von Programmen gelten, daß das Funktionsergebnis von S[[W]] = _ ist. Hierfür ist wiederum
eine Änderung der Definition des Statements notwendig.
S: Statement -> Environment_ -> Environment_
mit :
Environment_ = (Identifier -> Integer_)_