§ 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 cardinalityof 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 cangive 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 considerationstell 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 canbe 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

§ CPOs

  • Given a partial order (P,)(P, \leq). assume we have a subset QPQ \subseteq P. A least upper bound uu of QQ is an element that is the smallest element in PPwhich is larger than every element in QQ.
  • A subset QQ of PP is called as a chain if its elements can be put into order.That is, there is a labelling of elements of QQ into q1,q2,,qnq1, q2, \dots, qn suchthat q1q2qnq1 \leq q2 \leq \dots \leq qn.

§ CCPOs

  • A partially ordered set is called as a chain complete partial order ifeach chain has a least upper bound.
  • This is different from a lattice, where each subset has a least upper bound.
  • Every ccpo has a minimal element given by completion()=completion(\emptyset) = \bot.
  • TODO: example of ccpo that is not a lattice

§ 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 isonly 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 continuousonly works for CCPOs.
  • The composition of continuous functions of chain-complete partiallyordered 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