Semantics of loops [dt-001V]

Armed with the \textbf {fix} operator, we can return to our semantics of \mathsf {while} loops from § [dt-0006] and § [dt-000R], and at last define their semantics without relying on dubious recursive definitions: \begin {array}{l} \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C} = \textbf {fix}(f)\\[0.5em] \qquad \text {where}\; f(X)\ \sigma \; \triangleq \; \begin {cases} X\ (\llbracket c \rrbracket _\mathcal {C}\ \sigma ) & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \sigma & \text {otherwise} \end {cases} \end {array}

Proof that f is continuous is technically required but is omitted here.