Last time we defined the denotational semantics of IMP: In this lecture we’ll prove Kleene’s fixpoint theorem, which shows that the fixed point used to define the semantics of while commands exists, and work through examples of reasoning using the denotational semantics.
Kleene’s Fixpoint Theorem
Definition (Scott Continuity). A function from to is said to be Scott-continuous if for every chain we have It is not hard to show that if is Scott continuous, then it is also monotonic—that is, implies The proof of this fact is left as an exercise. Theorem (Kleene Fixpoint). LetFbea Scott-continuous function. The least fixed point of is Proof. Let First, we will prove that 𝑋 is a fixed point of 𝐹—that is, 𝐹(𝑋)= 𝑋. Notice that , we calculate as follows: Second, we will show that X is the least fixed point of . Suppose that is some other arbitrary fixed point of . By induction, we can easily show that for all . For the base case, is and we trivially have . For the inductive case, we assume that and prove that By our inductive hypothesis and the fact that is monotone, we have that As is a fixed point we also have and so
Then, since every element of the chain is a subset of immediately we have that their union, . Hence, is the least (with respect to ) fixed point of .
Reasoning
One of the key advantages of using denotational semantics compared to operational semantics is that proofs of equivalence can be carried out directly by simply calculating the denotations of programs and then arguing that they are identical. This is in contrast to operational techniques, where one must reason explicitly about low-level transitions and derivations involving ad hoc abstract machines.
As an example, to show that and are equivalent, we can calcuate as follows, using standard facts about partial functions, relations, and sets as convenient in the proof itself.
Next, consider the command . By the definition of the denotational semantics, this is equal to where By the Kleene fixpoint theorem we have that . It is straightforward to show by induction that since the guard is , for all we have It follows that , which is just .
As an exercise, calcuate using the same technique.
