Fixed points [dt-000U]

From recursion to fixed points [dt-000R]

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.

DefinitionFixed point [dt-000S]

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

Monotonicity is insufficient [dt-000T]

Exercise [dt-000Q]

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

  2. Give an example of a poset A and a monotonic function f : A \rightarrow A such that f has multiple fixed points.

    3. Solution.

Problem.

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]

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]

    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]

    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]

    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.

    DefinitionDirected set [dt-0010]

    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.

    ExamplePower sets are directed [dt-0011]

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

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

      TheoremChain → Directed [dt-0012]

      All non-empty chains are directed.

      Proof.

      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.

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

        TheoremAlternative characterisation of directedness [dt-0014]

        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.

        • ⇐: 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]

        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]

        DefinitionLeast upper bound [dt-0017]

        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:

        1. It is an upper bound: \forall x \in X.\ x \sqsubseteq y
        2. 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\}.

        CorollaryProperties of \sqcup [dt-0018]

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

        TheoremPointedness via lubs [dt-0019]

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

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

                Complete partial orders [dt-001E]

                DefinitionComplete partial order [dt-001D]

                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:

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

                AsideOther kinds of completeness [dt-001F]

                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]

                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.

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

                Solution.

                RemarkLubs 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]

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

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

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

                      4. Solution.

                    Continuity and Fixed Points [dt-001I]

                    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,

                    1. \bigsqcup \{ f(x) \mid x \in X \} exists, and
                    2. 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.

                    TheoremContinuity implies monotonicity [dt-001L]

                    All continuous functions are monotonic.

                    Proof.

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

                    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.

                    TheoremAlternative characterisation of continuity [dt-001O]

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

                    1. f is monotonic, and
                    2. 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.

                      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]

                          1. What is \textbf {fix}(\mathsf {id}) where \mathsf {id} is the identity function on \mathbb {B}_\bot ?

                            Solution.

                          2. What is \textbf {fix}(\kappa _\mathit {F}) where \kappa _\mathit {F} is the constant function that always returns \mathit {F}?

                            Solution.

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

                          Context

                            Lecture. Domain theory › Semantics and recursion [dt-0005]