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 ))))$ :

ExampleAscending 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.

DefinitionChain [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$