Recursively defined programs [dt-0006]
Suppose we extended the \mathcal {C} language with a while loop construct: \mathcal {C}\; \Coloneqq \; \cdots \mid \mathsf {while}\ \mathcal {B}\ \mathsf {do}\ \mathcal {C}\ \mathsf {od} The intuitive way to assign a semantics would be to use a recursive function: \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C}\ \sigma \; = \; \begin {cases} \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C}\ (\llbracket c \rrbracket _\mathcal {C}\ \sigma ) & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \sigma & \text {otherwise} \end {cases} However, such an equation is not a good definition. If we consider the trivial infinite loop program L \triangleq \mathsf {while}\ \mathsf {true}\ \mathsf {do}\ \mathsf {skip}\ \mathsf {od}, and compute its semantics, we end up with: \llbracket \mathsf {while}\ \mathsf {true}\ \mathsf {do}\ \mathsf {skip}\ \mathsf {od} \rrbracket _\mathcal {C}\ \sigma \; = \; \llbracket \mathsf {while}\ \mathsf {true}\ \mathsf {do}\ \mathsf {skip}\ \mathsf {od} \rrbracket _\mathcal {C}\ \sigma This equation is satisfied by any function \Sigma \rightarrow \Sigma , so it doesn't tell us which function corresponds to the program L.
More generally, allowing our functions to be (generally) recursive causes these issues. The loop program L gives rise to the recursive equation \ell (x) = \ell (x), which has an infinite number of solutions.
If we add recursion to our programming language, we could have programs that give rise to more complex recursive equations like f(x) = f(x) + 1. By contrast to \ell (x), f(x) has no solutions (assuming f(x) operates on integers).