Definition. Fixed point [dt-000S]

Liam O'Connor

A value $x$ is a fixed point of a function $f$ if $f(x) = x$ .

Context

Fixed points [dt-000U]

Liam O'Connor

From recursion to fixed points [dt-000R]

Liam O'Connor

Consider our recursive $\mathsf {while}$ loop semantics from § [dt-0006]: $\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}$ How do we ensure that solutions exist for such recursive equations? And, if multiple solutions exist, how do we decide which one to pick? To address these questions, let's factor out everything in our definition except the recursion into a separate (higher-order) function: $\begin {array}{l} \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C} = f(\llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C}) \\[0.5em] \qquad \text {where}\; f(X)\ \sigma \; \triangleq \; \begin {cases} X\ (\llbracket c \rrbracket _\mathcal {C}\ \sigma ) & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \sigma & \text {otherwise} \end {cases} \end {array}$ Looking at it this way, we can see that any solution to this equation must be an element of our semantic domain $X \in \mathbf {C}$ such that $f(X) = X$ . In other words, the problem of finding solutions to our recursive equations can be cast as the problem of finding a fixed point for non-recursive higher-order functions.

Definition. Fixed point [dt-000S]

Liam O'Connor

A value $x$ is a fixed point of a function $f$ if $f(x) = x$ .

Monotonicity is insufficient [dt-000T]

Liam O'Connor

Exercise. [dt-000Q]

Liam O'Connor

Give an example of a poset A and a monotonic function f : A \rightarrow A such that f doesn't have a fixed point.
Solution.
- Liam O'Connor
In the poset $(\mathbb {N},\leq )$ , the function $f(x) = x + 1$ has no fixed points.
Give an example of a poset $A$ and a monotonic function $f : A \rightarrow A$ such that $f$ has multiple fixed points.

Solution.

Liam O'Connor

In the poset $(\mathbb {N},\leq )$ , the function $f(x) = x$ has infinitely many fixed points.

Problem.

Liam O'Connor

Not all monotonic functions on posets have fixed points, and some have multiple fixed points!

So, requiring our functions to be monotonic is insufficient to guarantee that a single "best" solution exists.

Chains and Unfolding [dt-000Y]

with contributions from Liam O'Connor

Intuitively, recursive programs are executed by "unfolding" as much as necessary to get a result. We would like to characterise our domains to ensure that solutions always exist, and to allow us to pick the solutions that are "minimal" in the sense that they rely on a minimal amount of unfolding.

After converting a recursive program into a non-recursive monotonic higher order function $f$ , the fixed point we desire would intuitively be the limit of the ascending Kleene chain of $f$ , i.e. $f(f(f(f(\dots ))))$ :

Example. Ascending Kleene chain [dt-000X]

Given a pointed poset $(X,\subseteq )$ and a monotonic function $f : X \rightarrow X$ , the ascending Kleene chain is the $\omega$ -chain: $\bot \sqsubseteq f(\bot ) \sqsubseteq f(f(\bot )) \sqsubseteq f(f(f(\bot ))) \sqsubseteq \cdots$ Because $\bot$ is the bottom element, we know that $\bot \sqsubseteq f(\bot )$ . Each subsequent step in the chain exists because of monotonicity.

Each successive element of this chain is another "unfolding" of the recursion.

Definition. Chain [dt-000V]

Liam O'Connor

A chain in a poset $X$ is a totally ordered subset of $X$ . That is, a subset $Y \subseteq X$ is a chain iff: $\forall x, y \in Y.\; x \sqsubseteq y \lor y \sqsubseteq x$

Definition. $\omega$ -chain [dt-000W]

Liam O'Connor

An $\omega$ -chain is a chain that is countable. In other words, it is a sequence of elements $x_{i \in \mathbb {N}}$ such that: $x_0 \sqsubseteq x_1 \sqsubseteq x_2 \sqsubseteq x_3 \dots$

From chains to directed sets [dt-000Z]

with contributions from Liam O'Connor

While $\omega$ -chains are technically sufficient for denotational semantics, for our purposes it is a little more convenient to think in terms of directed sets rather than chains.

Definition. Directed set [dt-0010]

Liam O'Connor

Formally, a non-empty subset $Y \subseteq X$ of a poset $(X,\sqsubseteq )$ is directed iff: $\forall x, y \in Y.\ \exists z \in Y.\ x \sqsubseteq z \land y \sqsubseteq z$

The

z

above is an upper bound of

x

and

y

. Hence, a non-empty set is directed iff every pair of values has an upper bound in the set.

Intuitively, directed sets are "going somewhere" — given two elements we can always find a "greater" one in the set.

Example. Power sets are directed [dt-0011]

The power set of any set $X$ is directed under $\subseteq$ .

Below: $\cal {P}(\{1,2,3\})$ :

Theorem. Chain → Directed [dt-0012]

Liam O'Connor

All non-empty chains are directed.

Proof.

Liam O'Connor

Let $C$ be a chain. Then, given two elements $x,y \in C$ we know from totality that either $x \sqsubseteq y$ or $y \sqsubseteq x$ . If $x \sqsubseteq y$ , then $y$ is the upper bound, otherwise $x$ is the upper bound.

Definition. Consistent subset [dt-0013]

A subset $Y \subseteq X$ of a poset $X$ is consistent iff $\exists x \in X.\ \forall y \in Y.\ y \sqsubseteq x$ Such an $x$ is called an upper bound of $Y$ .

Theorem. Alternative characterisation of directedness [dt-0014]

Liam O'Connor

A subset $Y \subseteq X$ of a poset $X$ is directed iff every finite subset of $Y' \subseteq Y$ has an upper bound in $Y$ .

Proof.

Liam O'Connor

⇐: Every pair of elements $x,y \in Y$ has an upper bound simply by taking the upper bound of the set $\{x,y\}.$
⇒: Given a finite set $X = \{x_1,x_2,\dots , x_n\}$ , we can show it has an upper bound by an inductive process, first taking the upper bound of $x_1$ and $x_2$ , and then taking the upper bound of that an $x_3$ and so on until we have an upper bound for the whole set. This induction works because the set $X$ is finite.

Corollary. [dt-0015]

Liam O'Connor

From Theorem [dt-0014] we can see that a finite set $S$ is directed iff it has a top element $\top$ , i.e. $\forall x \in S.\ x \sqsubseteq \top$ .

Least upper bounds [dt-0016]

Liam O'Connor

Definition. Least upper bound [dt-0017]

Liam O'Connor

Let $X \subseteq Y$ be a subset of a poset $Y$ . An element $y \in Y$ is a least upper bound (or lub) for $X$ iff:

It is an upper bound: $\forall x \in X.\ x \sqsubseteq y$
It is less than any other upper bound: $\forall y' \in Y.\ (\forall x \in X. x \sqsubseteq y') \Rightarrow y \sqsubseteq y'$

It follows that lubs are unique if they exist. We write the lub of a set

X

as

\bigsqcup X

, and usually write

x \sqcup y

as a shorthand for

\bigsqcup \{x,y\}

.

Corollary. Properties of $\sqcup$ [dt-0018]

Liam O'Connor

When lubs exist, the binary $\sqcup$ operator is idempotent, commutative, and associative. Also, we have that $x \sqsubseteq y$ iff $x \sqcup y = y$ .

Theorem. Pointedness via lubs [dt-0019]

Liam O'Connor

A poset $Y$ is pointed iff $\bigsqcup \emptyset$ exists, as the lub of an empty set is just the bottom element in the poset, i.e. $\bigsqcup \emptyset = \bot$ .

Information intuition [dt-001A]

When the poset $Y$ from Definition [dt-0017] is ordered by our information ordering, the intuition of the lub $\bigsqcup X$ is that it combines all of the information content of all the elements of $X$ but it does not add any additional information (hence least).

Example. Lubs in the domain $\mathbb {B}_\bot \times \mathbb {B}_\bot$ [dt-001B]

$(\bot , \mathit {F}) \sqcup (\mathit {T},\bot ) = (\mathit {T},\mathit {F})$
$(\bot , \mathit {F}) \sqcup (\bot ,\bot ) = (\bot ,\mathit {F})$
$(\bot , \mathit {F}) \sqcup (\mathit {T}, \mathit {T})$ does not exist.

Exercise. [dt-001C]

What is the lub operator on subsets $X \subseteq \mathbb {N}$ of the poset $(\mathbb {N},\leq )$ ?

Solution.

The lub operator is maximum.

Complete partial orders [dt-001E]

Liam O'Connor

Definition. Complete partial order [dt-001D]

Liam O'Connor

A complete partial order or cpo (more specifically a directed complete partial order or dcpo) is a poset where lubs exist for the empty set and for all directed subsets. That is, a cpo is a poset $A$ such that:

$A$ has a bottom element $\bot \in A$ , that is the lub of the empty set, and
$\bigsqcup X$ exists for all directed $X \subseteq A$ .

Aside. Other kinds of completeness [dt-001F]

Liam O'Connor

In Definition [dt-001D] we defined cpos in terms of directed completeness. We may consider chain completeness instead, where, rather than require lubs for every directed subset of our poset $A$ , we require lubs for every chain $X \subseteq A$ . We know from Theorem [dt-0012] that all chains are directed, so every directed complete cpo is also chain complete. It is also known that every chain complete cpo is also directed complete, so the notions are equivalent, although the proof is non-trivial, relying on transfinite induction (see these lecture notes for details).

If we weaken our completeness requirement to require lubs only for the countable $\omega$ -chains and not necessarily all chains, we get what is called an $\omega$ -cpo. All $\omega$ -chains are chains and are therefore directed, but not all chains are $\omega$ -chains.

Working with just $\omega$ -cpos is common in denotational semantics practice, but working with directed completeness simplifies some of the properties we will discuss later.

Exercise. [dt-001G]

Liam O'Connor

For each of the following posets, determine if it is a cpo or not. If it is, describe the lubs. If it is not, give a directed set which has no lub.

A finite pointed poset
$(\mathcal {P}(S), \subseteq )$ for some set $S$
$(\mathbb {N},\leq )$
$(\mathbb {N} \cup \{\infty \}, \leq )$
$([0,1] \subseteq \mathbb {R}, \leq )$
$([0,1) \subseteq \mathbb {R}, \leq )$
$(\mathbb {Q}, \leq )$
A flat domain $S_\bot$ for some set $S$ .

Solution.

Liam O'Connor

A finite pointed poset is a cpo, as all directed subsets will be finite and therefore have a lub.
$(\mathcal {P}(S), \subseteq )$ is a cpo as the lub is just the union.
$(\mathbb {N},\leq )$ is not a cpo, as the $\omega$ -chain $1 \leq 2 \leq 3 \leq \cdots$ has no lub.
$(\mathbb {N} \cup \{\infty \}, \leq )$ is a cpo, as $\infty$ is the lub of any non-repeating chain.
$([0,1] \subseteq \mathbb {R}, \leq )$ is a cpo with maximum as the lub.
$([0,1) \subseteq \mathbb {R}, \leq )$ is not a cpo, as the set $\{0.9,0.99,0.999,\dots \}$ has a lub of $1 \notin [0,1)$ .
$(\mathbb {Q}, \leq )$ is not a cpo, and not just because it lacks a lub for $\mathbb {Q}$ itself, but also it doesn't contain $\sqrt {2}$ , which can be expressed as the lub of an infinite sequence of rational approximations.
A flat domain $S_\bot$ for some set $S$ is a cpo, as the largest chains have two elements, and we always pick the non- $\bot$ one as the lub.

Remark. Lubs of chains [dt-001H]

The limit of the ascending Kleene chain of a monotonic function $f : X \rightarrow X$ is the same as the least upper bound of the set $\{ f^n(\bot ) \mid n \in \mathbb {N}\}$ (where $f^n$ is the $n$ -fold self-composition of the function $f$ ). If we require that our semantic domain $X$ is a cpo, we know that this limit exists.

Thesis.

Our semantic domains are cpos, ensuring the presence of these limits.

Exercise. [dt-001X]

Liam O'Connor

Show that if A and B are posets and X \subseteq A \times B is directed (by the ordering in Construction [dt-000E]), then the subsets \pi _0(X) \subseteq A and \pi _1(X) \subseteq B (defined below) are also directed. \begin {array}{lcl} \pi _0(X) & = & \{ a \in A \mid \exists b \in B.\ (a,b) \in X \}\\ \pi _1(X) & = & \{ b \in B \mid \exists a \in A.\ (a,b) \in X \}\\ \end {array}
Solution.
- Liam O'Connor
Given two elements $x,y \in \pi _0(X)$ , we know that there exists $b_x, b_y \in B$ such that $(x,b_x) \in X$ and $(y,b_y) \in X$ . Because $X$ is directed, we can conclude that there exists an upper bound $(z, b_z) \in X$ where $x \sqsubseteq z$ and $y \sqsubseteq z$ . As $z \in \pi _0(X)$ , $z$ is an upper bound in $\pi _0(X)$ for both $x$ and $y$ and thus $\pi _0(X)$ is directed. The proof for $\pi _1$ is analogous.
Give an example of a set X \subseteq \{\top ,\bot \}\times \{\top ,\bot \} such that \pi _0(X) and \pi _1(X) are directed, but X is not.
Solution.
- Liam O'Connor
$X = \{(\top ,\bot ), (\bot ,\top )\}$ is not directed as the two elements are not comparable, but $\pi _0(X) = \pi _1(X) = \{\top ,\bot \}$ which is directed as $\bot \sqsubseteq \top$ .
Show that if $A$ and $B$ are cpos and $X \subseteq A \times B$ is directed, then $\bigsqcup X = \left (\bigsqcup \pi _0(X), \bigsqcup \pi _1(X)\right )$ Note: Together with $\bot _{A\times B} = (\bot _A, \bot _B)$ this shows that the Cartesian product of two cpos is itself a cpo.

Solution.

Liam O'Connor

Let $(x,y) = \left (\bigsqcup \pi _0(X), \bigsqcup \pi _1(X)\right )$ . Because of the ordering in Construction [dt-000E], $(x,y)$ is certainly a upper bound of the directed set $X$ . To show it is the least upper bound, assume for the sake of contradiction that $(x,y)$ is not the least upper bound of $X$ . Then, there must be a $(v,w)\sqsubset (x,y)$ such that $\forall x \in X.\ x \sqsubseteq (v,w)$ . But then, $v$ would be a lesser upper bound for $\pi _0(X)$ than $x$ , which is supposed to be the lub. Thus there is a contradiction, and $(x,y)$ must be the lub of $X$ .

Continuity and Fixed Points [dt-001I]

with contributions from Liam O'Connor

By choosing a cpo for our semantic domain, we can ensure that the Kleene chain has a limit. However, it is not guaranteed that the limit we find will be a fixed point to our monotonic function $f$ .

Problem. Monotonicity is insufficient [dt-001K]

Liam O'Connor

Consider this monotonic function $g$ defined over a cpo $(\mathbb {R} \cup \{\infty ,-\infty \}, \leq )$ : $g(x) = \begin {cases} \tan ^{-1} x & \text {if}\ x < 0\\ 1 & \text {otherwise} \end {cases}$ Note this function is not continuous at 0. Starting from our $\bot$ element $-\infty$ , we can see that the limit of the ascending Kleene chain is $0$ : $\begin {array}{lcl} g(-\infty ) & = & -\frac {\pi }{2}\\ g(-\frac {\pi }{2}) & = & -1\\ g(-1) & \approx & -0.78\\ \end {array}$ But $g(0) = 1$ ! — the lub of the Kleene chain is not a fixed point!

To address this problem, we shall strengthen our requirement on functions from mere monotonicity to continuity.

Definition. Continuity [dt-001J]

Liam O'Connor

A function $f : A \rightarrow B$ on cpos $A$ and $B$ is continuous iff for all directed $X \subseteq A$ ,

$\bigsqcup \{ f(x) \mid x \in X \}$ exists, and
$f(\bigsqcup X) = \bigsqcup \{ f(x) \mid x \in X \}$ , i.e., $f$ preserves lubs.

The intuition behind continuity is that "nothing is suddenly invented at infinity": our function will behave analogously at the limit as it does for each element in our chain.

Theorem. Continuity implies monotonicity [dt-001L]

Liam O'Connor

All continuous functions are monotonic.

Proof.

Liam O'Connor

Consider two elements $x, y$ of a cpo where $x \sqsubseteq y$ . Then $\{x,y\}$ is directed with a lub of $y$ . By the second condition in Definition [dt-001J], we get $f(y) = f(x) \sqcup f(y)$ which is equivalent to $f(x) \sqsubseteq f(y)$ .

Example. Monotonic but not continuous [dt-001M]

Liam O'Connor

Consider this function from $\mathbb {N} \cup \{\infty \} \rightarrow \{\top ,\bot \}$ , defined by: $f(x) = \begin {cases} \bot & \text {if}\ x \in \mathbb {N}\\ \top & \text {otherwise} \end {cases}$ This function is monotonic, but, taking $X = \mathbb {N}$ (which is a directed subset of the cpo $\mathbb {N} \cup \{\infty \}$ ), then $f(\bigsqcup \mathbb {N}) = f(\infty ) = \top$ , but $\bigsqcup \{ f(n) \mid n \in \mathbb {N} \} = \bigsqcup \{ \bot \} = \bot$ . Thus, this function is not continuous.

Exercise. [dt-001N]

Liam O'Connor

Show that if a function on cpos $f : A \rightarrow B$ is monotonic, then $\bigsqcup \{ f(x) \mid x \in X \}$ exists for any directed $X \subseteq A$ (i.e.the first condition for continuity in Definition [dt-001J]).

Hint: It suffices to show that $\{ f(x) \mid x \in X \} \subseteq B$ is directed.

Solution.

Liam O'Connor

Because $B$ is a cpo, it suffices to show that $\{ f(x) \mid x \in X \} \subseteq B$ is directed. Let $a,b \in \{ f(x) \mid x \in X \}$ . Let $x_a, x_b \in X$ be the values that $f$ maps to $a$ and $b$ respectively, i.e. $f(x_a) = a$ and $f(x_b) = b$ . Because $X$ is directed, an upper bound of $x_a$ and $x_b$ exists in $X$ . Call this upper bound $x_c$ . Because $x_a \sqsubseteq x_c$ and $x_b \sqsubseteq x_c$ , we know that $f(x_a) = a \sqsubseteq f(x_c)$ and $f(x_b) = b \sqsubseteq f(x_c)$ by monotonicity of $f$ . Also, $f(x_c) \in \{ f(x) \mid x \in X \}$ because $x_c \in X$ . Therefore, because two arbitrary elements in $\{ f(x) \mid x \in X \}$ have an upper bound within the set, the set $\{ f(x) \mid x \in X \}$ is directed.

Theorem. Alternative characterisation of continuity [dt-001O]

Liam O'Connor

A function $f : A \rightarrow B$ on cpos $A$ and $B$ is continuous iff:

$f$ is monotonic, and
$f(\bigsqcup X) = \bigsqcup \{ f(x) \mid x \in X \}$ , for all directed $X \subseteq A$

Proof.

Liam O'Connor

The second condition here is identical to that of Definition [dt-001J]. The monotonicity requirement is equivalent to the first condition of Definition [dt-001J], with one direction shown by Theorem [dt-001L], and the other shown by the solution of Exercise [dt-001N].

Thesis.

Computable functions are continuous functions on cpos.

Exercise. [dt-001W]

Liam O'Connor

Show that if a function $f : A \rightarrow B$ on cpos $A$ and $B$ is monotonic and $A$ is finite, then $f$ is continuous.

Hint: Finite directed sets contain their lub

Solution.

Liam O'Connor

Because of Theorem [dt-001O], it suffices to show the second condition of continuity, as $f$ is monotonic.

Because $A$ is finite, any directed subset $X \subseteq A$ is also finite, and therefore $\bigsqcup X \in X$ . Because $f$ is monotone, $f(x) \sqsubseteq f (\bigsqcup X)$ for all $x \in X$ .

The solution to Exercise [dt-001N] shows that $\{f(x) \mid x \in X\}$ is directed and therefore contains its upper bound $c$ . Because $f$ is monotone, $f(\bigsqcup X)$ must be $c$ (else it would contradict the above).

Therefore $\bigsqcup \{f(x) \mid x \in X\} = f (\bigsqcup X)$ , as required.

Theorem. The Kleene fixed point theorem [dt-001P]

Let $(S, \sqsubseteq )$ be a cpo and $f : S \rightarrow S$ be a continuous function. Then the lub of the Kleene chain $\bigsqcup _{n\in \mathbb {N}}f^{n}(\bot )$ is the least fixed point of $f$ .

Proof.

We apply continuity to show that it is a fixed point: $\begin {array}{lclr} f(\bigsqcup _{n \in \mathbb {N}} f^n(\bot ) ) & = & \bigsqcup _{n \in \mathbb {N}} f(f^n(\bot )) & \text {(continuity)} \\[0.5em] &=& \bigsqcup _{n \in \mathbb {N}} f^{n+1}(\bot )\\[0.5em] &=& \bigsqcup _{n=1,2\dots }f^{n}(\bot ) &\qquad \text {(reindexing)}\\[0.5em] &=& \bot \sqcup \bigsqcup _{n=1,2\dots }f^{n}(\bot )\\[0.5em] &=&\bigsqcup _{n\in \mathbb {N}}f^{n}(\bot )\\[0.5em] \end {array}$ To see that it is the least fixed point: Let $y$ be a fixed point of $f$ . We know that $\bot \sqsubseteq y$ by definition of $\bot$ . Taking $f$ of both sides, we get $f(\bot ) \sqsubseteq y$ . We can continue this inductively and thus we know that, for all $n \in \mathbb {N}$ , $f^n(\bot ) \sqsubseteq y$ . Because $y$ is, therefore, an upper bound of the ascending Kleene chain, it must also be at least as large as the lub of that chain.

Definition. The $\textbf {fix}$ operator [dt-001Q]

Liam O'Connor

Let $\textbf {fix}(f)$ denote the least fixed point of the continuous function $f$ , that is $\bigsqcup _{n\in \mathbb {N}}f^{n}(\bot )$ , guaranteed to exist by Theorem [dt-001P].

Exercise. [dt-001S]

Liam O'Connor

What is \textbf {fix}(\mathsf {id}) where \mathsf {id} is the identity function on \mathbb {B}_\bot ?
Solution.
- Liam O'Connor
$\bigsqcup \{ \bot , \mathsf {id}(\bot ), \mathsf {id}(\mathsf {id}(\bot )), \dots \} = \bot$
What is \textbf {fix}(\kappa _\mathit {F}) where \kappa _\mathit {F} is the constant function that always returns \mathit {F}?
Solution.
- Liam O'Connor
$\bigsqcup \{ \bot , \kappa _F(\bot ), \kappa _F(\kappa _F(\bot )), \dots \} = \mathit {F}$
What is \textbf {fix}(f) where \begin {array}{l} f : [\mathbb {N}_\bot ] \rightarrow [\mathbb {N}_\bot ]\\ f(x) = 1::x \end {array} (where [\mathbb {N}_\bot ] denotes Haskell-style lazy lists of \mathbb {N}_\bot )?
Solution.
- Liam O'Connor
$\bigsqcup \{ \bot , 1::\bot , 1::1::\bot , \dots \} = 1::1::1::\cdots$ Here $\textbf {fix}(f)$ would be the semantics of the recursive definition $\mathsf {ones} = 1 :: \mathsf {ones}$ .

Backlinks

Exercise. [dt-000Q]

Liam O'Connor

Give an example of a poset A and a monotonic function f : A \rightarrow A such that f doesn't have a fixed point.
Solution.
- Liam O'Connor
In the poset $(\mathbb {N},\leq )$ , the function $f(x) = x + 1$ has no fixed points.
Give an example of a poset $A$ and a monotonic function $f : A \rightarrow A$ such that $f$ has multiple fixed points.

Solution.

Liam O'Connor

In the poset $(\mathbb {N},\leq )$ , the function $f(x) = x$ has infinitely many fixed points.

Chains and Unfolding [dt-000Y]

with contributions from Liam O'Connor

Intuitively, recursive programs are executed by "unfolding" as much as necessary to get a result. We would like to characterise our domains to ensure that solutions always exist, and to allow us to pick the solutions that are "minimal" in the sense that they rely on a minimal amount of unfolding.

After converting a recursive program into a non-recursive monotonic higher order function $f$ , the fixed point we desire would intuitively be the limit of the ascending Kleene chain of $f$ , i.e. $f(f(f(f(\dots ))))$ :

Example. Ascending Kleene chain [dt-000X]

Given a pointed poset $(X,\subseteq )$ and a monotonic function $f : X \rightarrow X$ , the ascending Kleene chain is the $\omega$ -chain: $\bot \sqsubseteq f(\bot ) \sqsubseteq f(f(\bot )) \sqsubseteq f(f(f(\bot ))) \sqsubseteq \cdots$ Because $\bot$ is the bottom element, we know that $\bot \sqsubseteq f(\bot )$ . Each subsequent step in the chain exists because of monotonicity.

Each successive element of this chain is another "unfolding" of the recursion.

Definition. Chain [dt-000V]

Liam O'Connor

A chain in a poset $X$ is a totally ordered subset of $X$ . That is, a subset $Y \subseteq X$ is a chain iff: $\forall x, y \in Y.\; x \sqsubseteq y \lor y \sqsubseteq x$

Definition. $\omega$ -chain [dt-000W]

Liam O'Connor

An $\omega$ -chain is a chain that is countable. In other words, it is a sequence of elements $x_{i \in \mathbb {N}}$ such that: $x_0 \sqsubseteq x_1 \sqsubseteq x_2 \sqsubseteq x_3 \dots$

Continuity and Fixed Points [dt-001I]

with contributions from Liam O'Connor

By choosing a cpo for our semantic domain, we can ensure that the Kleene chain has a limit. However, it is not guaranteed that the limit we find will be a fixed point to our monotonic function $f$ .

Problem. Monotonicity is insufficient [dt-001K]

Liam O'Connor

Consider this monotonic function $g$ defined over a cpo $(\mathbb {R} \cup \{\infty ,-\infty \}, \leq )$ : $g(x) = \begin {cases} \tan ^{-1} x & \text {if}\ x < 0\\ 1 & \text {otherwise} \end {cases}$ Note this function is not continuous at 0. Starting from our $\bot$ element $-\infty$ , we can see that the limit of the ascending Kleene chain is $0$ : $\begin {array}{lcl} g(-\infty ) & = & -\frac {\pi }{2}\\ g(-\frac {\pi }{2}) & = & -1\\ g(-1) & \approx & -0.78\\ \end {array}$ But $g(0) = 1$ ! — the lub of the Kleene chain is not a fixed point!

To address this problem, we shall strengthen our requirement on functions from mere monotonicity to continuity.

Definition. Continuity [dt-001J]

Liam O'Connor

A function $f : A \rightarrow B$ on cpos $A$ and $B$ is continuous iff for all directed $X \subseteq A$ ,

$\bigsqcup \{ f(x) \mid x \in X \}$ exists, and
$f(\bigsqcup X) = \bigsqcup \{ f(x) \mid x \in X \}$ , i.e., $f$ preserves lubs.

The intuition behind continuity is that "nothing is suddenly invented at infinity": our function will behave analogously at the limit as it does for each element in our chain.

Theorem. Continuity implies monotonicity [dt-001L]

Liam O'Connor

All continuous functions are monotonic.

Proof.

Liam O'Connor

Consider two elements $x, y$ of a cpo where $x \sqsubseteq y$ . Then $\{x,y\}$ is directed with a lub of $y$ . By the second condition in Definition [dt-001J], we get $f(y) = f(x) \sqcup f(y)$ which is equivalent to $f(x) \sqsubseteq f(y)$ .

Example. Monotonic but not continuous [dt-001M]

Liam O'Connor

Consider this function from $\mathbb {N} \cup \{\infty \} \rightarrow \{\top ,\bot \}$ , defined by: $f(x) = \begin {cases} \bot & \text {if}\ x \in \mathbb {N}\\ \top & \text {otherwise} \end {cases}$ This function is monotonic, but, taking $X = \mathbb {N}$ (which is a directed subset of the cpo $\mathbb {N} \cup \{\infty \}$ ), then $f(\bigsqcup \mathbb {N}) = f(\infty ) = \top$ , but $\bigsqcup \{ f(n) \mid n \in \mathbb {N} \} = \bigsqcup \{ \bot \} = \bot$ . Thus, this function is not continuous.

Exercise. [dt-001N]

Liam O'Connor

Show that if a function on cpos $f : A \rightarrow B$ is monotonic, then $\bigsqcup \{ f(x) \mid x \in X \}$ exists for any directed $X \subseteq A$ (i.e.the first condition for continuity in Definition [dt-001J]).

Hint: It suffices to show that $\{ f(x) \mid x \in X \} \subseteq B$ is directed.

Solution.

Liam O'Connor

Because $B$ is a cpo, it suffices to show that $\{ f(x) \mid x \in X \} \subseteq B$ is directed. Let $a,b \in \{ f(x) \mid x \in X \}$ . Let $x_a, x_b \in X$ be the values that $f$ maps to $a$ and $b$ respectively, i.e. $f(x_a) = a$ and $f(x_b) = b$ . Because $X$ is directed, an upper bound of $x_a$ and $x_b$ exists in $X$ . Call this upper bound $x_c$ . Because $x_a \sqsubseteq x_c$ and $x_b \sqsubseteq x_c$ , we know that $f(x_a) = a \sqsubseteq f(x_c)$ and $f(x_b) = b \sqsubseteq f(x_c)$ by monotonicity of $f$ . Also, $f(x_c) \in \{ f(x) \mid x \in X \}$ because $x_c \in X$ . Therefore, because two arbitrary elements in $\{ f(x) \mid x \in X \}$ have an upper bound within the set, the set $\{ f(x) \mid x \in X \}$ is directed.

Theorem. Alternative characterisation of continuity [dt-001O]

Liam O'Connor

A function $f : A \rightarrow B$ on cpos $A$ and $B$ is continuous iff:

$f$ is monotonic, and
$f(\bigsqcup X) = \bigsqcup \{ f(x) \mid x \in X \}$ , for all directed $X \subseteq A$

Proof.

Liam O'Connor

The second condition here is identical to that of Definition [dt-001J]. The monotonicity requirement is equivalent to the first condition of Definition [dt-001J], with one direction shown by Theorem [dt-001L], and the other shown by the solution of Exercise [dt-001N].

Thesis.

Computable functions are continuous functions on cpos.

Exercise. [dt-001W]

Liam O'Connor

Show that if a function $f : A \rightarrow B$ on cpos $A$ and $B$ is monotonic and $A$ is finite, then $f$ is continuous.

Hint: Finite directed sets contain their lub

Solution.

Liam O'Connor

Because of Theorem [dt-001O], it suffices to show the second condition of continuity, as $f$ is monotonic.

Because $A$ is finite, any directed subset $X \subseteq A$ is also finite, and therefore $\bigsqcup X \in X$ . Because $f$ is monotone, $f(x) \sqsubseteq f (\bigsqcup X)$ for all $x \in X$ .

The solution to Exercise [dt-001N] shows that $\{f(x) \mid x \in X\}$ is directed and therefore contains its upper bound $c$ . Because $f$ is monotone, $f(\bigsqcup X)$ must be $c$ (else it would contradict the above).

Therefore $\bigsqcup \{f(x) \mid x \in X\} = f (\bigsqcup X)$ , as required.

Theorem. The Kleene fixed point theorem [dt-001P]

Let $(S, \sqsubseteq )$ be a cpo and $f : S \rightarrow S$ be a continuous function. Then the lub of the Kleene chain $\bigsqcup _{n\in \mathbb {N}}f^{n}(\bot )$ is the least fixed point of $f$ .

Proof.

We apply continuity to show that it is a fixed point: $\begin {array}{lclr} f(\bigsqcup _{n \in \mathbb {N}} f^n(\bot ) ) & = & \bigsqcup _{n \in \mathbb {N}} f(f^n(\bot )) & \text {(continuity)} \\[0.5em] &=& \bigsqcup _{n \in \mathbb {N}} f^{n+1}(\bot )\\[0.5em] &=& \bigsqcup _{n=1,2\dots }f^{n}(\bot ) &\qquad \text {(reindexing)}\\[0.5em] &=& \bot \sqcup \bigsqcup _{n=1,2\dots }f^{n}(\bot )\\[0.5em] &=&\bigsqcup _{n\in \mathbb {N}}f^{n}(\bot )\\[0.5em] \end {array}$ To see that it is the least fixed point: Let $y$ be a fixed point of $f$ . We know that $\bot \sqsubseteq y$ by definition of $\bot$ . Taking $f$ of both sides, we get $f(\bot ) \sqsubseteq y$ . We can continue this inductively and thus we know that, for all $n \in \mathbb {N}$ , $f^n(\bot ) \sqsubseteq y$ . Because $y$ is, therefore, an upper bound of the ascending Kleene chain, it must also be at least as large as the lub of that chain.

Definition. The $\textbf {fix}$ operator [dt-001Q]

Liam O'Connor

Let $\textbf {fix}(f)$ denote the least fixed point of the continuous function $f$ , that is $\bigsqcup _{n\in \mathbb {N}}f^{n}(\bot )$ , guaranteed to exist by Theorem [dt-001P].

Exercise. [dt-001S]

Liam O'Connor

What is \textbf {fix}(\mathsf {id}) where \mathsf {id} is the identity function on \mathbb {B}_\bot ?
Solution.
- Liam O'Connor
$\bigsqcup \{ \bot , \mathsf {id}(\bot ), \mathsf {id}(\mathsf {id}(\bot )), \dots \} = \bot$
What is \textbf {fix}(\kappa _\mathit {F}) where \kappa _\mathit {F} is the constant function that always returns \mathit {F}?
Solution.
- Liam O'Connor
$\bigsqcup \{ \bot , \kappa _F(\bot ), \kappa _F(\kappa _F(\bot )), \dots \} = \mathit {F}$
What is \textbf {fix}(f) where \begin {array}{l} f : [\mathbb {N}_\bot ] \rightarrow [\mathbb {N}_\bot ]\\ f(x) = 1::x \end {array} (where [\mathbb {N}_\bot ] denotes Haskell-style lazy lists of \mathbb {N}_\bot )?
Solution.
- Liam O'Connor
$\bigsqcup \{ \bot , 1::\bot , 1::1::\bot , \dots \} = 1::1::1::\cdots$ Here $\textbf {fix}(f)$ would be the semantics of the recursive definition $\mathsf {ones} = 1 :: \mathsf {ones}$ .

Definition. Fixed points of endofunctors on $\mathbf {Cpo}$ [dt-004W]

Liam O'Connor

A fixed point of an endofunctor on cpos $\mathcal {F}$ is a cpo $\mathcal {F}$ such that $\mathcal {F}(A) \simeq A$ .

Note.

Liam O'Connor

In Scott's approach, which we follow here, our fixed points are up to isomorphism (suitable for languages with isorecursive types), but there are other approaches where they are equalities (suitable for languages with equirecursive types).

From recursion to fixed points [dt-000R]

Liam O'Connor

Consider our recursive $\mathsf {while}$ loop semantics from § [dt-0006]: $\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}$ How do we ensure that solutions exist for such recursive equations? And, if multiple solutions exist, how do we decide which one to pick? To address these questions, let's factor out everything in our definition except the recursion into a separate (higher-order) function: $\begin {array}{l} \llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C} = f(\llbracket \mathsf {while}\ b\ \mathsf {do}\ c\ \mathsf {od} \rrbracket _\mathcal {C}) \\[0.5em] \qquad \text {where}\; f(X)\ \sigma \; \triangleq \; \begin {cases} X\ (\llbracket c \rrbracket _\mathcal {C}\ \sigma ) & \text {if}\ \llbracket b \rrbracket _\mathcal {B}\ \sigma = \mathit {T} \\ \sigma & \text {otherwise} \end {cases} \end {array}$ Looking at it this way, we can see that any solution to this equation must be an element of our semantic domain $X \in \mathbf {C}$ such that $f(X) = X$ . In other words, the problem of finding solutions to our recursive equations can be cast as the problem of finding a fixed point for non-recursive higher-order functions.

Problem. Monotonicity is insufficient [dt-001K]

Liam O'Connor

Consider this monotonic function $g$ defined over a cpo $(\mathbb {R} \cup \{\infty ,-\infty \}, \leq )$ : $g(x) = \begin {cases} \tan ^{-1} x & \text {if}\ x < 0\\ 1 & \text {otherwise} \end {cases}$ Note this function is not continuous at 0. Starting from our $\bot$ element $-\infty$ , we can see that the limit of the ascending Kleene chain is $0$ : $\begin {array}{lcl} g(-\infty ) & = & -\frac {\pi }{2}\\ g(-\frac {\pi }{2}) & = & -1\\ g(-1) & \approx & -0.78\\ \end {array}$ But $g(0) = 1$ ! — the lub of the Kleene chain is not a fixed point!

Monotonicity is insufficient [dt-000T]

Liam O'Connor

Exercise. [dt-000Q]

Liam O'Connor

Give an example of a poset A and a monotonic function f : A \rightarrow A such that f doesn't have a fixed point.
Solution.
- Liam O'Connor
In the poset $(\mathbb {N},\leq )$ , the function $f(x) = x + 1$ has no fixed points.
Give an example of a poset $A$ and a monotonic function $f : A \rightarrow A$ such that $f$ has multiple fixed points.

Solution.

Liam O'Connor

In the poset $(\mathbb {N},\leq )$ , the function $f(x) = x$ has infinitely many fixed points.

Problem.

Liam O'Connor

Not all monotonic functions on posets have fixed points, and some have multiple fixed points!

So, requiring our functions to be monotonic is insufficient to guarantee that a single "best" solution exists.

Theorem. The Kleene fixed point theorem [dt-001P]

Let $(S, \sqsubseteq )$ be a cpo and $f : S \rightarrow S$ be a continuous function. Then the lub of the Kleene chain $\bigsqcup _{n\in \mathbb {N}}f^{n}(\bot )$ is the least fixed point of $f$ .

Proof.

We apply continuity to show that it is a fixed point: $\begin {array}{lclr} f(\bigsqcup _{n \in \mathbb {N}} f^n(\bot ) ) & = & \bigsqcup _{n \in \mathbb {N}} f(f^n(\bot )) & \text {(continuity)} \\[0.5em] &=& \bigsqcup _{n \in \mathbb {N}} f^{n+1}(\bot )\\[0.5em] &=& \bigsqcup _{n=1,2\dots }f^{n}(\bot ) &\qquad \text {(reindexing)}\\[0.5em] &=& \bot \sqcup \bigsqcup _{n=1,2\dots }f^{n}(\bot )\\[0.5em] &=&\bigsqcup _{n\in \mathbb {N}}f^{n}(\bot )\\[0.5em] \end {array}$ To see that it is the least fixed point: Let $y$ be a fixed point of $f$ . We know that $\bot \sqsubseteq y$ by definition of $\bot$ . Taking $f$ of both sides, we get $f(\bot ) \sqsubseteq y$ . We can continue this inductively and thus we know that, for all $n \in \mathbb {N}$ , $f^n(\bot ) \sqsubseteq y$ . Because $y$ is, therefore, an upper bound of the ascending Kleene chain, it must also be at least as large as the lub of that chain.

Definition. The $\textbf {fix}$ operator [dt-001Q]

Liam O'Connor

Let $\textbf {fix}(f)$ denote the least fixed point of the continuous function $f$ , that is $\bigsqcup _{n\in \mathbb {N}}f^{n}(\bot )$ , guaranteed to exist by Theorem [dt-001P].