Semantics of Loops Actually we can view Iwhile b do clcomm as a solution for this equation: while b do c]lcomm =lif b then (c;while b do c)else skipllcomm (while do com)(commftrue otherwise That is,Iwhile b do cllcomm is a fixed-point of Fsex-zi.oez{&iclameneaeg=twue otherwise However,,not every Fe(E→∑t)→（∑→∑！）has a fixed-point,, and some may have more than one. Example:for any o',o.is a solution for l[while true do x :=x+1]comm- Denotational SemanticsSemantics of Loops Actually we can view ~while b do ccomm as a solution for this equation: ~while b do ccomm σ = ~if b then (c ; while b do c) else skipcomm σ = ( (~while b do ccomm)y (~ccomm σ) if ~bboolexp σ = true σ otherwise That is, ~while b do ccomm is a fixed-point of F def = λf ∈ Σ → Σ⊥. λσ ∈ Σ. ( fy(~ccomm σ) if ~bboolexp σ = true σ otherwise However, not every F ∈ (Σ → Σ⊥) → (Σ → Σ⊥) has a fixed-point, and some may have more than one. Example: for any σ 0 , λσ. σ0 is a solution for ~while true do x := x + 1comm. Denotational Semantics