Why Least Fixpoints

April, 2021

Why does denotational semantics care about least fixpoints, as opposed to say greatest or some other fixpoints? Answer: because it's least fixpoints that capture our operational intuitions of code. Read on for an example. Thanks to Alejandro Lopez for the helpful comments and corrections.

In denotational semantics we're interested in a denotation function that maps program terms to mathematical functions. For example, we might say that the denotation of the statement A := A + 1 is the function on stores that maps location A to its successor I use the following notation for store updates: \( s' = s[A \rightarrow v] \) is the store such that \( s'(A) = v \) and \( s'(l) = s(l) \) for \( l \neq A \). : $$ [[ A := A + 1 ]] = \lambda s. s[A \rightarrow s(A) + 1] $$ To represent nontermination we use a bottom element \( \bot \), so denotations are functions \( Store_{\bot} \rightarrow Store_{\bot} \), where \( Store = Id \rightarrow Nat \) \( Store_{\bot} \) then contains all the functions in \( Store \), plus \( \bot \). . This way, an infinite loop is denoted by the function that sends any store to \( \bot \): $$ [[ while\ (true)\ do\ skip ]] = \lambda s. \bot $$

Fixpoints arise naturally when looking at denotations of loops. Our operational intuition of loops motivates the desideratum $$ [[ while \ (B)\ do \ S ]] = [[ if\ (B)\ then\ (S;\ while\ (B)\ do\ S)\ else\ skip ]] $$ Now let \( L = while \ (B)\ do \ S \), getting $$ [[ L ]] = [[ if\ (B)\ then (S; L) else \ skip ]] $$ Computing the denotations (which I haven't explained how to do) we get $$ [[ L ]] = \lambda s. if\ ([[ B ]] s)\ then\ [[ L ]] ([[ S ]] s)\ else\ s $$ The important part is that \( [[L]] \) appears in both sides of the equation. Here we do the usual trick where instead of the equation above we write the corresponding functional $$ F = \lambda f. \lambda s. if\ ([[ B ]] s)\ then\ f([[ S ]] s)\ else\ s $$ Notice the denotation \( [[ L ]] \) we're looking for is such that $$ [[ L ]] = F([[ L ]]) $$ a fixpoint!

Ok so now we know that fixpoints are useful for modelling loops, but why do we care specifically about least fixpoints? The reason is that there's a theorem that tells us that least fixpoints can be computed in a way that's compatible with the operational semantics of loops. But it's also interesting to examine what goes wrong if we were to use e.g. greatest fixpoints.

Consider the loop while (A = 0) do skip (call it \( L \)). Operationally, we would say that the loop terminates iff the initial value of \( A \) is non-zero. Denotationally, we'd like to say that \( [[ L ]] \) is the function that sends every store where \( A \) is zero to \( \bot \), and leaves all other stores unchanged: $$ [[ L ]] = \lambda s.\ if\ ([[ A = 0 ]] s)\ then\ \bot\ else\ s $$ Indeed, this is a fixpoint, because $$ \begin{align*} F([[ L ]]) &= \lambda s.\ if ([[ A = 0 ]] s)\ then\ [[ L ]] ([[ skip ]] s)\ else\ s \\ &= \lambda s.\ if ([[ A = 0 ]] s )\ then\ [[ L ]](s)\ else\ s \\ &= \lambda s.\ if ([[ A = 0 ]] s )\ then\ (if ([[ A = 0 ]] s)\ then\ \bot \ else \ s)\ else\ s \\ &= \lambda s.\ if ([[ A = 0 ]] s )\ then\ \bot\ else\ s \\ &= [[ L ]] \end{align*} $$

But the above is not the only fixpoint. Consider a denotation that makes \( L \) the identity: $$ [[ L ]]' = \lambda s. s $$ This is also a fixpoint, because $$ \begin{align*} F([[ L ]]') &= \lambda s.\ if ([[ A = 0 ]] s)\ then\ [[ L ]]' ([[ skip ]] s)\ else\ s \\ &= \lambda s.\ if ([[ A = 0 ]] s )\ then\ [[ L ]]'(s)\ else\ s \\ &= \lambda s.\ if ([[ A = 0 ]] s )\ then\ s\ else\ s \\ &= \lambda s. s \\ &= [[ L ]]' \end{align*} $$ Additionally, we have \( [[ L ]] < [[ L ]]' \) (although I haven't defined what less than means in this context) because the former sends stores with \( A = 0 \) to \( \bot \), whereas the latter leaves them unchanged. But this second interpretation of the loop as the identity is clearly wrong! Moral of the story: we really do want least fixpoints, and not just any old fixpoint.

References