Denotational semantics of while programs

The denotational semantics intends to view the program behaviour from a more abstract aspect. Two programs are hard to compare, if we take into account all the smaller steps of program execution. Rather than evaluating a program from a given state step by step, the denotational semantics renders a denotation to the program, which is a partial function from states to states. We consider two programs equal if their denotations coincide. More formally,

The question is whether we are able to give a more direct way to compute the denotations of program than the operational approach. Before giving the denotations of programs, we should give the denotations of arithmetic- and Boolean expressions, but this is straightforward, so we ignore this task. We turn directly to defining the denotations of programs. The denotation of a program C is the partial function , where is the subset of on which is defined. In what follows, we may use the more convenient notation rather than . Moreover, to make our notation more illustrative, we write , if , and , if .

Definition 16.

Remark 17. We remark that in the above definition the composition of relations is used in a manner somewhat different from the treatment of some of the textbooks. If A, B and C are arbitrary sets and is a relation over , and is a relation over , then in a large number of the textbooks the composition is denoted by . To facilitate readability, however, we distinguish the notation of the composition reflecting a different order of the components: we use instead of , as detailed in the Appendix.

In Definition 16 the least fixpoint of an operator is determined. By the Kanster-Tarski theorem it exists provided is continuous.

Lemma 18. is continuous.

Let us calculate the denotational semantics of the program of Example 13. As before, let C denote the whole program, denote the loop and denote the body of the loop.

Example 19.

where are the approximations of according to Theorem 142. Let us calculate the values of :

Continuing in this way we obtain that

Thus

So far we have defined two different approaches to the meanings of programs. The question arises naturally how these approaches are connected. We state and prove the following theorem about the relation of the two approaches.

Theorem 20. The operational and denotational meanings of programs coincide. More precisely, for every program C,

Proof.

  • () Assume , that is, . The proof goes by induction on the length of the reduction sequence.

    • If , the statement trivially holds.

    • Assume , then we can distinguish several subcases.

      • : then we have for some , and . Moreover, the reduction sequences and are strictly shorter than n. By induction hypothesis, and . By Definition 16, this implies .

      • : assume . Hence, . This involves, by induction hypothesis, . The case for is treated similarly, and, by Definition 16, we obtain the result.

      • : assume . Then . By induction hypothesis we obtain . Let . Then , which is again in . Definition 16 gives the result.

  • () The proof goes by induction on the complexity of C. If C is skip, or an assignment, then the result is immediate.

    • : assume . Then, by Definition 16, we have and for some . By the induction hypothesis, and . This gives , which was to be proved.

    • : let , assume . Then , thus . Otherwise and . By Definition 12, the result follows.

    • : let , assume . Then , where

      Let us consider the , , .

      By Theorem 142, . We prove by induction on n that .

      1. : by Definition 12 the assertion trivially holds.

      2. with : assume we have the result for k. Let and for some with . Then, by the assumption for n and by induction hypothesis for , we have and , which, by Definitions 5 and 16, implies the result.

We should observe that if we use the notation of the previous chapter we can reformulate the appearance of as

Additionally, we prove another handy characterization of the denotational semantics of the while loop.

Lemma 21. .

Proof. Let and , where . We prove that

which, by Lemma 143, gives the result. To this end, we prove by induction on n that

where and are the usual approximations of and , respectively. For the statement is trivial. Assume for some , and the equation holds for k. Then

By this, the proof is complete.