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.

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

Proof.

Problem. Monotonicity is insufficient [dt-001K]

Definition. Continuity [dt-001J]

Theorem. Continuity implies monotonicity [dt-001L]

Proof.

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

Exercise. [dt-001N]

Solution.

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

Proof.

Thesis.

Exercise. [dt-001W]

Solution.

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

Proof.

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

Exercise. [dt-001S]

Solution.

Solution.

Solution.