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.
ProblemMonotonicity is insufficient [dt-001K]
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.
DefinitionContinuity [dt-001J]
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.
TheoremContinuity implies monotonicity [dt-001L]
All continuous functions are monotonic.
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).Proof.
ExampleMonotonic but not continuous [dt-001M]
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]
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.
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.
TheoremAlternative characterisation of continuity [dt-001O]
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.
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]
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.
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.
TheoremThe 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.
DefinitionThe \textbf {fix} operator [dt-001Q]
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]
- What is \textbf {fix}(\mathsf {id}) where \mathsf {id} is the identity function on \mathbb {B}_\bot ?
Solution.
\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.
\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.
\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}.