§ Crash course on DCPO: formalizing lambda calculus

In lambda calculus, we often see functions of the form λxx(x)\lambda x \rightarrow x(x). We would like a way to associate a "natural" mathematical object to such a function. The most obvious choice for lambda calculus is to try to create a set VV of values which contains its own function space: (VV)V(V \rightarrow V) \subseteq V. This seems to ask for a set whose cardinality is such that VV=V|V|^|V| = |V|, which is only possible if V=1|V| = 1, ie VV is the trivial set {}\{ * \}. However, we know that lambda calculus has at least two types of functions: functions that terminate and those that don't terminate. Hence the trivial set is not a valid solution. However, there is a way out. The crucial insight is one that I shall explain by analogy:
  • We can see that the cardinality of R\mathbb R is different from the cardinality of the space of functions over it, RR\mathbb R \rightarrow \mathbb R.
  • However, "the set of all functions" isn't really something mathematicians consider. One would most likely consider "the set of all continuous functions" RR\mathbb R \rightarrow \mathbb R.
  • Now note that a function that is continuous over the reals is determined by its values at the rationals . So, rather than giving me a continus function f:RRf: \mathbb R \rightarrow \mathbb R, you can give me a continuous function f:QRf': \mathbb Q \rightarrow \mathbb R which I can Cauchy-complete, to get a function completion(f):RR=f\texttt{completion}(f') : \mathbb R \rightarrow \mathbb R = f.
  • Now, cardinality considerations tell us that:
RQ=(20)0=200=20=R|\mathbb R^\mathbb Q| = (2^{\aleph_0})^{\aleph_0} = 2^{\aleph_0 \cdot \aleph_0} = 2^\aleph_0 = |R|
  • We've won! We have a space R\mathbb R whose space of continuous functions RR\mathbb R \rightarrow \mathbb R is isomorphic to R\mathbb R.
  • We bravely posit: all functions computed by lambda-calculus are continuous! Very well. This leaves us two questions to answer to answer: (1) over what space? (2) with what topology? The answers are (1) a space of partial orders (2) with the Scott topology

§ Difference between DCPO theory and Domain theory

  • A DCPO (directed-complete partial order) is an algebraic structure that can be satisfied by some partial orders. This definition ports 'continuity' to partial orders.
  • A domain is an algebraic structure of even greater generality than a DCPO. This attempts to capture the fundamental notion of 'finitely approximable'.

§ Computation as fixpoints of continuous functions

§ Posets, (least) upper bounds

  • A partial order (P,)(P, \leq) is a set equipped with a reflexive, transitive, relation \leq such that xyx \leq y and yxy \leq x implies x=yx = y.
  • A subset DPD \subseteq P is said to have an upper bound uDPu_D \in P iff for all dDd \in D, it is true that duDd \leq u_D.
  • An upper bound is essentially a cone over the subset DD in the category PP.
  • A subset DPD \subseteq P has a least upper bound lDl_D iff (1) lDl_D is an upper bound of DD, and (2) for every upper bound uDu_D, it is true that lDuDl_D \leq u_D
  • Least upper bounds are unique, since they are essentially limits of the set DD when DD is taken as a thin category

§ Directed Sets

  • A subset DPD \subseteq P is said to be directed iff for every finite subset SDS \subseteq D, SS has a upper bound dSd_S in DD. That is, the set DD is closed under the upper bound of all of its subsets.
  • Topologically, we can think of it as being closure , since the upper bound is sort of a "limit point" of the subset, and we are saying that DD has all of its limit points.
  • Categorically, this means that DPD \subseteq P taken as a subcategory of PP has cones over all finite subsets. (See that we do not ask for limits/least upper bounds over all finite subsets, only cones/upper bounds).
  • We can think of the condition as saying that the information in DD is internally consistent: for any two facts, there is a third fact that "covers" them both.
  • slogan: internal consistency begets an external infinite approximation.
  • QUESTION: why not ask for countable limits as well?
  • QUESTION: why upper bounds in DD? why not external upper bounds in PP?
  • QUESTION: why only upper bounds in DD? why not least upper bounds in DD?
  • ANSWER: I think the point is that as long as we ask for upper bounds, we can pushforward via a function ff, since the image of a directed set will be directed.

§ Directed Complete Partial Order ( DCPO)

  • A poset is said to be directed complete iff every directed set DPD \subseteq P has a least upper bound in PP.
  • Compare to chain complete, CCPO, where every chain has a LUB.
  • QUESTION: why not postulate that the least upper bound must be in DD?
  • In a DCPO, for a directed set DD, denote the upper bound by D\cup D.

§ Monotonicity and Continuity

  • A function f:PQf: P \to Q between posets is said to be monotone iff ppp \leq p' implies that f(p)f(p)f(p) \leq f(p').
  • A function f:PQf: P \to Q is continuous, iff for every directed set DPD \subseteq P, it is true that f(D)=f(D)f(\cup D) = \cup f(D).
  • This has the subtle claim that the image of a directed set is directed.

§ Monotone map

  • A function from PP to QQ is said to be monotone if pp    f(p)f(p)p \leq p' \implies f(p) \leq f(p').
  • Composition of monotone functions is monotone.
  • The image of a chain wrt a monotone function is a chain.
  • A monotone function need not preserve least upper bounds . Consider:
f:2N2Nf(S){SSisfiniteSU{0}S is infinite f: 2^{\mathbb N} \rightarrow 2^{\mathbb N} f(S) \equiv \begin{cases} S & \text{$S$} is finite \\ S U \{ 0 \} &\text{$S$ is infinite} \end{cases}
This does not preserve least-upper-bounds. Consider the sequence of elements:
A1={1},A2={1,2},A3={1,2,3},,An={1,2,3,,n} A_1 = \{ 1\}, A_2 = \{1, 2\}, A_3 = \{1, 2, 3\}, \dots, A_n = \{1, 2, 3, \dots, n \}
The union of all AiA_i is N\mathbb N. Each of these sets is finite. Hence f({1})={1}f(\{1 \}) = \{1 \}, f({1,2})={1,2}f(\{1, 2 \}) = \{1, 2\} and so on. Therefore:
f(Ai)=f(N)=N{0}f(Ai)=Ai=N f(\sqcup A_i) = f(\mathbb N) = \mathbb N \cup \{ 0 \}\\ \sqcup f(A_i) = \sqcup A_i = \mathbb N

§ Continuous function

  • A function is continous if it is monotone and preserves all LUBs. This is only sensible as a definition on ccpos, because the equation defining it is: lub . f = f . lub, where lub: chain(P) \rightarrow P. However, for lubto always exist, we need P to be a CCPO. So, the definition of continuous only works for CCPOs.
  • The composition of continuous functions of chain-complete partially ordered sets is continuous.

§ Fixpoints of continuous functions

The least fixed point of a continous function f:DDf: D \rightarrow D is:
FIX(f)lub({fn():n0})\texttt{FIX}(f) \equiv \texttt{lub}(\{ f^n(\bot) : n \geq 0 \})

§ \leq as implication

We can think of bab \leq a as b    ab \implies a. That is, bb has more information than aa, and hence implies aa.

§ References