Go backward to Example Go up to Top Go forward to Reasoning about Least Fixed Points

While Loops

Representation by finite subfunctions

C[[while B do C]] = |_|{
    lambda s._|_,
    lambda s.B[[B]]s -> _|_ [] s,
    lambda s.B[[B]]s -> (B[[B]](C[[C]]s) -> _|_ [] C[[C]]s)
         [] s,
    lambda s.B[[B]]s -> (B[[B]](C[[C]]s) ->
        (B[[B]](C[[C]](C[[C]]s)) -> _|_
        [] C[[C]](C[[C]]s)) [] C[[C]]s) [] s, ...}
= |_|{
    C[[diverge]],
    C[[if B then diverge else skip]],
    C[[if B then (C; if B then diverge else skip)
        else skip]],
    C[[if B then (C; if B then
            (C; if B then diverge else skip)
        else skip) else skip]], ...}

Loop iteration can be understood by sequence of non-iterating programs.