§ Crash course on DCPO: formalizing lambda calculus

In lambda calculus, we often see functions of the form λx→x(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: (V→V)⊆V(V \rightarrow V) \subseteq V. This seems to ask for a set whose cardinality is such that ∣V∣∣V∣=∣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, R→R\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" R→R\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:R→Rf: \mathbb R \rightarrow \mathbb R, you can give me a continuous function f′:Q→Rf': \mathbb Q \rightarrow \mathbb R which I can Cauchy-complete, to get a function completion(f′):R→R=f\texttt{completion}(f') : \mathbb R \rightarrow \mathbb R = f.
  • Now, cardinality considerations tell us that:
∣RQ∣=(2ℵ0)ℵ0=2ℵ0⋅ℵ0=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 R→R\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

§ CPOs

  • Given a partial order (P,≤)(P, \leq). assume we have a subset Q⊆PQ \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 such that q1≤q2≤⋯≤qnq1 \leq q2 \leq \dots \leq qn.

§ CCPOs

  • A partially ordered set is called as a chain complete partial order if each 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 p≤p′  ⟹  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:2N→2Nf(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:D→Df: D \rightarrow D is:
FIX(f)≡lub({fn(⊥):n≥0})\texttt{FIX}(f) \equiv \texttt{lub}(\{ f^n(\bot) : n \geq 0 \})

§ ≤\leq as implication

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

§ References