Go up to Top Go forward to Recursive Function Definitions

Semantics of Loops

B: Boolean-expression
C: Command
...
C ::= ...| while B do C | ...
...
C[[while B do C]] =
    lambda s. B[[B]]s -> C[[while B do C]](C[[C]]s) [] s

Problem: meaning of a syntax phrase may be defined only in terms of its proper subparts.

C[[while B do C]] = w
    where w: Store_{_|_} -> Store_{_|_}
    w = lambda s. B[[B]]s -> w(C[[C]]s) [] s

Recursion in syntax exchanged for recursion in function notation!