Denotational Semantics of IMP without the Least Fixed Point

It has been too long since I wrote a blog post! Needless to say, parenthood, teaching, research, service, and my wonderful graduate students and post-docs have been keeping me busy. But with the Fall 2016 semester winding down I can sneak away for a bit and think.

But first, I have something to admit. My education in the theory of programming languages has a glaring hole in it. I only have a very basic understanding of Denotational Semantics despite having taking a course on Domain Theory in graduate school. I figured it would be fun to remedy this situation, and it might even be useful in the future. So my first step was to understand the denotational semantics of the IMP language, which is the starter language for most textbooks on denotational semantics. IMP is simply an imperative language with assignment statements, while loops, if statements, and arithmetic on integers. The IMP language has two syntactic categories, expressions and commands. The following is the syntax of IMP.

\[ \begin{array}{lrcl} \text{variables} & x \\ \text{numbers} & n & \in & \mathbb{N} \\ \text{unary operators}&u & ::= & \neg \\ \text{binary operators}&b & ::= & + \mid - \mid \times \mid \,=\, \\ \text{expressions} & e & ::= & n \mid x \mid u(e) \mid b(e,e)\\ \text{commands} & c & ::= & \mathtt{skip} \mid x := e \mid c ; c \mid \mathtt{if}\;e\;\mathtt{then}\;c\;\mathtt{else}\;c \\ & & \mid & \mathtt{while}\;e\;\mathtt{do}\;c \end{array} \]

As far as I can tell, for a semantics to be a denotational semantics it has to satisfy two properties.

• It is a mapping from abstract syntax (the program) to a mathematical object, which is just to say some precisely defined entity, that describes the observable behavior of the program. For example, the mathematical object could be a relation between a program's inputs and outputs.
• It is compositional, which means that the denotation of a particular language construct is defined in terms of the denotation of the syntactic sub-parts of the construct. For example, the meaning of a while loop is defined in terms of the meaning of its conditional and the meaning of its body.

For the expressions of IMP, it is straightforward to write down a denotational semantics, the following function \(E\). This \(E\) is no different from a recursively defined interpreter. In the following, we map expressions to natural numbers. Following custom, we use the brackets \([\!| e |\!]\) ask a kind of quote to distinguish abstract syntax from the surrounding mathematics. To handle variables, we also pass in a function \(\sigma\) from variables to numbers, which we call a state.

\begin{align*} E[\!| n |\!](\sigma) &= n \\ E[\!| x_i |\!](\sigma) &= \sigma(x) \\ E[\!| u(e) |\!](\sigma) &= [\!|u|\!]( E[\!|e|\!] ) \\ E[\!| b(e_1,e_2) |\!](\sigma) &= [\!|b|\!]( E[\!|e_1|\!], E[\!|e_2|\!]) \\ \\ E[\!| \neg |\!](n) &= \begin{cases} 1 & \text{if } n = 0 \\ 0 & \text{if } n \neq 0\end{cases} \\ E[\!| + |\!](n_1,n_2) &= n_1 + n_2 \\ E[\!| - |\!](n_1,n_2) &= n_1 - n_2 \\ E[\!| \times |\!](n_1,n_2) &= n_1 \times n_2 \\ E[\!| = |\!](n_1,n_2) &= \begin{cases} 1 & \text{if } n_1 = n_2 \\ 0 & \text{if } n_1 \neq n_2 \end{cases} \end{align*}

What do the commands of IMP have in common regarding what they do? They change a state to a new state. For example, if \(\sigma\) is the incoming state, then the assignment command \( x := 42 \) outputs a new state \(\sigma'\) which is the same as \(\sigma\) except that \(\sigma'(x) = 42\). In general, the denotation of a command, \(C[\!|c|\!]\), will be a relation on states, that is, a set of pairs that match up input states with their corresponding output states. We shall give the denotational semantics of commands, one construct as a time.

The meaning of the skip command is that it it doesn't change the state, so it relates each state to itself.

\[ C[\!| \mathtt{skip} |\!] = \{ (\sigma,\sigma) \mid \sigma \in \mathit{state} \} \]

The meaning of the assignment statement is to update the state to map the left-hand side variable to the result of the right-hand side expression. So the new state is a function that takes in a variable named \(y\) and returns \( [\!|e|\!](\sigma) \) if \(y=x\) and otherwise returns the same thing as \(\sigma\).

\begin{align*} C[\!| x := e |\!] &= \{ (\sigma, \sigma') \mid \sigma \in \mathit{state} \} \\ & \text{where } \sigma'(y) = \begin{cases} E[\!|e|\!](\sigma) & \text{if}\, y = x\\ \sigma(y) & \text{if}\, y \neq x \end{cases} \end{align*}

The meaning of two commands in sequence is just the meaning of the first followed by the meaning of the second.

\[ C[\!| c_1; c_2 |\!] = \{ (\sigma,\sigma'') \mid \exists \sigma'. (\sigma,\sigma') \in C[\!| c_1 |\!] \land (\sigma',\sigma'') \in C[\!| c_2 |\!] \} \]

The meaning of an if command depends on the conditional expression \(e\). If the \(e\) evaluates to 0, then the meaning of if is given by the else branch \(c_2\). Otherwise, the meaning of if is given by the then branch \(c_1\).

\[ C[\!| \mathtt{if}\, e \,\mathtt{then}\, c_1 \,\mathtt{else}\, c_2 |\!] = \left\{ (\sigma,\sigma') \middle| \begin{array}{l} (\sigma,\sigma') \in C[\!| c_2 |\!] & \text{if}\, E[\!|e|\!](\sigma) = 0 \\ (\sigma,\sigma') \in C[\!| c_1 |\!] & \text{if}\, E[\!|e|\!](\sigma) \neq 0 \end{array} \right\} \]

The meaning of the while command is the crux of the matter. This is normally where a textbook includes several pages of beautiful mathematics about monotone and continuous functions, complete partial orders, and least fixed points. We're going to bypass all of that.

The meaning of an while command is to map each starting state \(\sigma_0\) to an ending state \(\sigma_n\) obtained by iterating it's body command so long as the condition is non-zero. Pictorially, we have the following:

We define an auxiliary function named \(L\) to express the iterating of the loop. It takes as input the number of iterations of the loop, the denotation of the condition expression \(de\), and the denotation of the command \(dc\).

\begin{align*} L(0, de, dc) &= \{ (\sigma,\sigma) \mid de(\sigma) = 0 \} \\ L(1+n, de, dc) &= \{ (\sigma,\sigma'') \mid de(\sigma) \neq 0 \land \exists \sigma'. (\sigma,\sigma') \in dc \land (\sigma',\sigma'') \in L(n, de, dc) \} \end{align*}

The meaning of the while command is to relate any state \(\sigma\) to state \(\sigma'\) if \(L(n,[\!|e|\!],[\!|c|\!])\) relates \(\sigma\) to \(\sigma'\) for some \(n\).

\[ C[\!| \mathtt{while}\, e \,\mathtt{do}\, c |\!] = \{ (\sigma,\sigma') \mid \exists n.\, (\sigma,\sigma') \in L(n,E[\!|e|\!],C[\!|c|\!]) \} \]

At this point I'm worried that this is so simple that it couldn't possibly be correct. A good way to check is to prove that it is equivalent to the standard big-step semantics for IMP, which we shall do now.

Equivalence to the Standard Big-Step Semantics

The big-step semantics for the IMP language is a three-place relation on a command, a starting state, and the final state, which we shall write \(c\mid\sigma\Downarrow\sigma'\). It is defined inductively by the following rules.

\begin{gather*} \frac{}{\mathtt{skip} \mid \sigma \Downarrow \sigma} \\[2ex] \frac{\sigma'(y) = \begin{cases} E[\!|e|\!](\sigma) & \text{if}\, y = x\\ \sigma(y) & \text{if}\, y \neq x \end{cases}}{ x := e \mid \sigma \Downarrow \sigma'} \qquad \frac{c_1 \mid \sigma \Downarrow \sigma' \quad c_2 \mid \sigma' \Downarrow \sigma''} {c_1 ; c_2 \mid \sigma \Downarrow \sigma''} \\[2ex] \frac{E[\!|e|\!](\sigma) = 0 \quad c_2 \mid \sigma \Downarrow \sigma' } {\mathtt{if}\,e\,\mathtt{then}\,c_1\,\mathtt{else}\,c_2 \mid \sigma \Downarrow \sigma'}\qquad \frac{E[\!|e|\!](\sigma) \neq 0 \quad c_1 \mid \sigma \Downarrow \sigma' } {\mathtt{if}\,e\,\mathtt{then}\,c_1\,\mathtt{else}\,c_2 \mid \sigma \Downarrow \sigma'}\\[2ex] \frac{E[\!|e|\!](\sigma) = 0} {\mathtt{while}\, e \,\mathtt{do}\, c \mid \sigma \Downarrow \sigma} \qquad \frac{E[\!|e|\!](\sigma) \neq 0 \quad c \mid \sigma \Downarrow \sigma' \quad \mathtt{while}\, e \,\mathtt{do}\, c \mid \sigma' \Downarrow \sigma''} {\mathtt{while}\, e \,\mathtt{do}\, c \mid \sigma \Downarrow \sigma''} \end{gather*}

(The big-step semantics is not denotational because the second rule for while is not compositional: the recursion is not on a proper sub-part but instead on the entire while command.)

We shall prove that the denotational semantics is equivalent to the big-step semantics in two steps.

1. The big-step semantics implies the denotational semantics. (completeness)
2. The denotation semantics implies the big-step semantics. (soundness)

Theorem (Completeness). If \(c \mid \sigma \Downarrow \sigma'\), then \((\sigma,\sigma') \in [\!|c|\!]\).
Proof. We proceed by induction on the derivation of \(c \mid \sigma \Downarrow \sigma'\). We have one case to consider per rule in the big-step semantics. (For the reader in a hurry: the case for while at the end is the only interesting one.)
Case: \[ \frac{}{\mathtt{skip} \mid \sigma \Downarrow \sigma} \] We need to show that \((\sigma,\sigma) \in [\!|\mathtt{skip}|\!]\), which is immediate from the definition of the denotational semantics.
Case: \[ \frac{\sigma'(y) = \begin{cases} E[\!|e|\!](\sigma) & \text{if}\, y = x\\ \sigma(y) & \text{if}\, y \neq x \end{cases}}{ x := e \mid \sigma \Downarrow \sigma'} \] We need to show that \((\sigma,\sigma') \in [\!|x := e|\!]\). Again this is immediate.
Case: \[ \frac{c_1 \mid \sigma \Downarrow \sigma' \quad c_2 \mid \sigma' \Downarrow \sigma''} {c_1 ; c_2 \mid \sigma \Downarrow \sigma''} \] We have two induction hypotheses: \((\sigma,\sigma') \in C[\!|c_1|\!]\) and \((\sigma',\sigma'') \in C[\!|c_2|\!]\). It follows (by definition) that \((\sigma,\sigma'') \in C[\!|c_1 ; c_2|\!]\).
Case: \[ \frac{E[\!|e|\!](\sigma) = 0 \quad c_2 \mid \sigma \Downarrow \sigma' } {\mathtt{if}\,e\,\mathtt{then}\,c_1\,\mathtt{else}\,c_2 \mid \sigma \Downarrow \sigma'}\qquad \] We have the induction hypothesis \((\sigma,\sigma') \in [\!|c_2|\!]\). Together with the condition expression evaluating to 0, we have \((\sigma,\sigma') \in C[\!|\mathtt{if}\,e\,\mathtt{then}\,c_1\,\mathtt{else}\,c_2|\!]\).
Case: \[ \frac{E[\!|e|\!](\sigma) \neq 0 \quad c_1 \mid \sigma \Downarrow \sigma' } {\mathtt{if}\,e\,\mathtt{then}\,c_1\,\mathtt{else}\,c_2 \mid \sigma \Downarrow \sigma'}\\[2ex] \] We have the induction hypothesis \((\sigma,\sigma') \in C[\!|c_1|\!]\). Together with the condition is non-zero, we have \((\sigma,\sigma') \in C[\!|\mathtt{if}\,e\,\mathtt{then}\,c_1\,\mathtt{else}\,c_2|\!]\).
Case: \[ \frac{E[\!|e|\!](\sigma) = 0} {\mathtt{while}\, e \,\mathtt{do}\, c \mid \sigma \Downarrow \sigma} \qquad \] From \(E[\!|e|\!](\sigma) = 0\) we have \((\sigma,\sigma) \in L(0,E[\!|e|\!],E[\!|c|\!]) \). Therefore \((\sigma,\sigma) \in C[\!|\mathtt{while}\, e \,\mathtt{do}\, c|\!]\).
Case: \[ \frac{E[\!|e|\!](\sigma) \neq 0 \quad c \mid \sigma \Downarrow \sigma' \quad \mathtt{while}\, e \,\mathtt{do}\, c \mid \sigma' \Downarrow \sigma''} {\mathtt{while}\, e \,\mathtt{do}\, c \mid \sigma \Downarrow \sigma''} \] We have the induction hypotheses \((\sigma,\sigma') \in C[\!|c|\!]\) and \((\sigma',\sigma'') \in C[\!|\mathtt{while}\, e \,\mathtt{do}\, c|\!]\). Unpacking the definition of the later, we have \( (\sigma',\sigma'') \in L(n,E[\!|e|\!],C[\!|c|\!]) \) for some \(n\). Therefore we have \( (\sigma,\sigma'') \in L(1+n,E[\!|e|\!],C[\!|c|\!]) \). So we conclude that \((\sigma,\sigma'') \in C[\!|\mathtt{while}\, e \,\mathtt{do}\, c|\!]\).
QED.

The other direction, that if the denotation of \(c\) relates \(\sigma\) to \(\sigma'\), then so does the big-step semantics, takes a bit more work. The proof will be by induction on the structure of \(c\). In the case for while we need to reason about the \(L\) function. We get to assume that \((\sigma,\sigma') \in L(n,E[\!|e|\!],C[\!|c|\!])\) for some \(n\) and we have the induction hypothesis that \(\forall \sigma \sigma'.\, (\sigma,\sigma') \in C[\!|c|\!] \to c \mid \sigma \Downarrow \sigma' \). Because \(L\) is recursive, we going to need a lemma about \(L\) and prove it by induction on the number of iterations.

Lemma If \((\sigma,\sigma') \in L(n,E[\!|e|\!],C[\!|c|\!])\) and \(\forall \sigma \sigma'.\, (\sigma,\sigma') \in [\!|c|\!] \to c \mid \sigma \Downarrow \sigma' \), then \(\mathtt{while}\, e \,\mathtt{do}\, c \mid \sigma \Downarrow \sigma' \).
Proof. The proof is by induction on \(n\).
Case \(n=0\). We have \((\sigma,\sigma') \in L(0,E[\!|e|\!],C[\!|c|\!])\), so \(\sigma = \sigma'\) and \(E[\!|e|\!](\sigma) = 0\). Therefore we can conclude that \(\mathtt{while}\, e \,\mathtt{do}\, c \mid \sigma \Downarrow \sigma'\).
Case \(n=1 + n'\). We have \((\sigma,\sigma') \in L(1+n',E[\!|e|\!],C[\!|c|\!])\), so \(E[\!|e|\!](\sigma) \neq 0\) and \( (\sigma,\sigma_1) \in C[\!|c|\!] \) and \( (\sigma_1,\sigma') \in L(n',E[\!|e|\!],C[\!|c|\!]) \) for some \(\sigma_1\). From the premise about \(c\), we have \(c \mid \sigma \Downarrow \sigma_1\). From the induction hypothesis, we have \(\mathtt{while}\, e \,\mathtt{do}\, c \mid \sigma_1 \Downarrow \sigma'\). Putting all of these pieces together, we conclude that \(\mathtt{while}\, e \,\mathtt{do}\, c \mid \sigma \Downarrow \sigma'\).
QED.

Theorem (Soundness). For any \(\sigma\) and \(\sigma'\), if \((\sigma,\sigma') \in C[\!|c|\!]\), then \(c \mid \sigma \Downarrow \sigma'\).
Proof. The proof is by induction on the structure of \(c\).
Case \(\mathtt{skip}\). From \((\sigma,\sigma') \in C[\!|\mathtt{skip}|\!]\) we have \(\sigma = \sigma'\) and therefore \(\mathtt{skip} \mid \sigma \Downarrow \sigma'\).
Case \(x:=e\). We have \[ \sigma'(y) = \begin{cases} E[\!|e|\!](\sigma) & \text{if}\, y = x\\ \sigma(y) & \text{if}\, y \neq x \end{cases} \] and therefore \(x := e \mid \sigma \Downarrow \sigma'\).
Case \(c_1 ; c_2\). We have \( (\sigma, \sigma_1) \in C[\!|c_1|\!]\) and \( (\sigma_1, \sigma') \in C[\!|c_2|\!]\) for some \(\sigma_1\). So by the induction hypothesis, we have \(c_1 \mid \sigma \Downarrow \sigma_1\) and \(c_2 \mid \sigma_1 \Downarrow \sigma'\), from which we conclude that \( c_1 ; c_2 \mid \sigma \Downarrow \sigma'\).
Case \(\mathtt{if}\,e\,\mathtt{then}\,c_1\,\mathtt{else}\,e_2\). We have two cases to consider, whether \(E[\!|e|\!](\sigma) = 0\) or not.

• Suppose \(E[\!|e|\!](\sigma) = 0\). Then \( (\sigma,\sigma') \in C[\!|c_2|\!] \) and by the induction hypothesis, \( c_2 \mid \sigma \Downarrow \sigma' \). We conclude that \( \mathtt{if}\,e\,\mathtt{then}\,c_1\,\mathtt{else}\,e_2 \mid \sigma \Downarrow \sigma' \).
• Suppose \(E[\!|e|\!](\sigma) \neq 0\). Then \( (\sigma,\sigma') \in C[\!|c_1|\!] \) and by the induction hypothesis, \( c_1 \mid \sigma \Downarrow \sigma' \). We conclude that \( \mathtt{if}\,e\,\mathtt{then}\,c_1\,\mathtt{else}\,e_2 \mid \sigma \Downarrow \sigma' \).

Case \(\mathtt{while}\, e \,\mathtt{do}\, c\). From \((\sigma,\sigma') \in C[\!|\mathtt{while}\, e \,\mathtt{do}\, c|\!]\) we have \( (\sigma,\sigma') \in L(n, E[\!|e|\!], C[\!|c|\!]) \). Also, by the induction hypothesis, we have that \( \forall \sigma \sigma'. \; (\sigma,\sigma') \in C[\!|c|\!] \to c \mid \sigma \Downarrow \sigma' \). By the Lemma about \(L\), we conclude that \(\mathtt{while}\, e \,\mathtt{do}\, c \mid \sigma \Downarrow \sigma'\).
QED.

Wow, the simple denotational semantics of IMP is correct!

The mechanization of all this in Coq is available here.

What about infinite loops?

Does this denotational semantics give meaning to programs with infinite loops, such as \[ \mathtt{while}\, 1 \,\mathtt{do}\, \mathtt{skip} \] The answer is yes, the semantics defines a total function from commands to relations, so every program gets a meaning. So the next question is which relation is the denotation of an infinite loop? Just like the fixed-point semantics, the answer is the empty relation. \[ C[\!|\mathtt{while}\, 1 \,\mathtt{do}\, \mathtt{skip} |\!] = \{ (\sigma,\sigma') \mid \exists n.\; (\sigma,\sigma') \in L(n, E[\!|1|\!], C[\!|\mathtt{skip}|\!]) \} = \emptyset \]

Comparison to using the least fixed point semantics

The standard denotational semantics for IMP defines the meaning of while in terms of the least fixed point of the following functional.

\[ W(de, dc)(dw) = \left\{ (\sigma,\sigma') \middle| \begin{array}{l} \sigma = \sigma' & \text{if } de(\sigma) = 0 \\ \exists \sigma_1, (\sigma,\sigma_1) \in dc \land (\sigma_1,\sigma') \in dw & \text{if } de(\sigma) \neq 0 \end{array} \right\} \]

One of the standard ways to compute the least fixed point of a functional \(F\) is from Kleene's fixpoint theorem, which says that the least fixed point of \(F\) is \[ \bigcup_{k=0}^{\infty} F^k(\emptyset) \] where \begin{align*} F^0(x) & = x \\ F^{k+1}(x) & = F (F^k(x)) \end{align*} So the traditional denotation of while is: \[ C[\!| \mathtt{while}\,e\,\mathtt{do}\,c |\!] = \bigcup_{k=0}^{\infty} W(E[\!|e|\!],C[\!|c|\!])^k(\emptyset) \] Applying the definition of infinitary union, we have \[ C[\!| \mathtt{while}\,e\,\mathtt{do}\,c |\!] = \{ (\sigma,\sigma') \mid \exists k.\; (\sigma,\sigma') \in W(E[\!|e|\!],C[\!|c|\!])^k(\emptyset) \} \] which starts to look similar to our definition. But they are not trivially equivalent.

Consider the following loop that counts down to zero. \[ \mathtt{while}\,\neg (x=0)\, \mathtt{do}\, x := x - 1 \] To talk about the semantics of this loop, we create the following abbreviations for some relations on states. \begin{align*} R_0 &= \{ (\sigma, \sigma) \mid \sigma(x) = 0 \} \\ R_1 &= \{ (\sigma, \sigma') \mid \sigma(x) = 1 \land \sigma'(x) = 0 \} \\ R_2 &= \{ (\sigma, \sigma') \mid \sigma(x) = 2 \land \sigma'(x) = 0 \} \\ R_3 &= \{ (\sigma, \sigma') \mid \sigma(x) = 3 \land \sigma'(x) = 0 \} \\ & \vdots \end{align*}

• If \(x=0\) in the initial state, the loop immediately terminates, so the final state is the same as the input state. This is \(R_0\).
• If \(x=1\) in the initial state, the loop executes one iteration, so the final state has \(x=0\). This is \(R_1\).
• If \(x=2\) in the initial state, the loop executes one iteration, so the final state has \(x=0\). This is \(R_2\).
• and so on.

The \(L\) function computes exactly these \(R\)'s. \begin{align*} L(0, E[\!| \neg (x = 0) |\!], C[\!| x := x - 1 |\!]) &= R_0 \\ L(1, E[\!| \neg (x = 0) |\!], C[\!| x := x - 1 |\!]) &= R_1 \\ L(2, E[\!| \neg (x = 0) |\!], C[\!| x := x - 1 |\!]) &= R_2 \\ L(3, E[\!| \neg (x = 0) |\!], C[\!| x := x - 1 |\!]) &= R_3\\ & \vdots \end{align*} The semantics of while given by \(L\) says that an initial state is related to a final state if it is possible to guess the iteration count \(n\) to pick out the appropriate line of \(L\) that relates the two states. \[ C[\!| \mathtt{while}\,e\,\mathtt{do}\,c |\!] = \{ (\sigma,\sigma') \mid \exists n.\, (\sigma,\sigma') \in L(n, [\!|e|\!],[\!|c|\!]) \} \] In contrast, Kleene's iteration incrementally builds up the union of all the \(R\)'s: \begin{align*} W(E[\!| \neg (x = 0) |\!], C[\!| x := x - 1 |\!])^0(\emptyset) &= \emptyset \\ W(E[\!| \neg (x = 0) |\!], C[\!| x := x - 1 |\!])^1(\emptyset) &= R_0\\ W(E[\!| \neg (x = 0) |\!], C[\!| x := x - 1 |\!])^2(\emptyset) &= R_0 \cup R_1 \\ W(E[\!| \neg (x = 0) |\!], C[\!| x := x - 1 |\!])^3(\emptyset) &= R_0 \cup R_1 \cup R_2 \\ & \vdots \end{align*} The semantics of while given by the least fixed point of \(W\) says that an initial state is related to a final state if, after a sufficient number of applications of \(W\), say \(k\), the two states are in the resulting union \(R_0 \cup \cdots \cup R_{k-1}\). \[ C[\!| \mathtt{while}\,e\,\mathtt{do}\,c |\!] = \{ (\sigma,\sigma') \mid \exists k.\; (\sigma,\sigma') \in W([\!|e|\!],[\!|c|\!])^k(\emptyset) \} \]

In general, \( L(n,E[\!|e|\!],C[\!|c|\!]) \) gives the denotation of the loop exactly when \(n\) is the number of iterations executed by the loop in a given initial state. In contrast, \( W(E[\!|e|\!],C[\!|c|\!])^k(\emptyset) \) produces the \(k\)th approximation of the loop's meaning, providing the appropriate initial/final states for up to \(k-1\) iterations of the loop.

However, these two algorithms are equivalent in the following sense.

Theorem (Equivalence to LFP semantics)

1. If \( (\sigma,\sigma') \in L(n,E[\!|e|\!],C[\!|c|\!]) \), then \( \exists k.\; (\sigma,\sigma') \in W(E[\!|e|\!],C[\!|c|\!])^k(\emptyset) \).
2. If \( (\sigma,\sigma') \in W(E[\!|e|\!],C[\!|c|\!])^k(\emptyset) \), then \( \exists n.\; (\sigma,\sigma') \in L(n,E[\!|e|\!],C[\!|c|\!]) \).

The first part is proved by induction on n. The second part is proved by induction on k. The full proofs are in the Coq development linked to above.

Parting Thoughts

• The traditional least fixed-point semantics is overkill for IMP.
• What makes this simple version work is the combination of choosing the denotation of commands to be relations on states (instead of functions on states) and the use of an existential for the number of loop iterations in the meaning of while.
• The IMP language is just a toy. As we consider more powerful language constructs such as functions, pointers, etc., at what point will we be forced to use the heavier-duty math of least fixed-points, continuous functions, etc.? I'm looking forward to finding out!