§ Crash course on DCPO: formalizing lambda calculus
In lambda calculus, we often see functions of the form λx→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 V of values
which contains its own function space: (V→V)⊆V. This
seems to ask for a set whose cardinality is such that ∣V∣∣V∣=∣V∣, which is
only possible if ∣V∣=1, ie V 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 is different from the cardinality of the space of functions over it, R→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.
- 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→R, you can give me a continuous function f′:Q→R which I can Cauchy-complete, to get a function completion(f′):R→R=f.
- Now, cardinality considerations tell us that:
∣RQ∣=(2ℵ0)ℵ0=2ℵ0⋅ℵ0=20ℵ=∣R∣
- We've won! We have a space R whose space of continuous functions R→R is isomorphic to 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,≤). assume we have a subset Q⊆P. A least upper bound u of Q is an element that is the smallest element in Pwhich is larger than every element in Q.
- A subset Q of P is called as a chain if its elements can be put into order. That is, there is a labelling of elements of Q into q1,q2,…,qn such that q1≤q2≤⋯≤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(∅)=⊥.
- TODO: example of ccpo that is not a lattice
§ Monotone map
- A function from P to Q is said to be monotone if p≤p′⟹f(p)≤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)≡{SSU{0}SisfiniteS is infinite
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}
The union of all Ai is N.
Each of these sets is finite.
Hence f({1})={1}, f({1,2})={1,2} and so on. Therefore:
f(⊔Ai)=f(N)=N∪{0}⊔f(Ai)=⊔Ai=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 lub
to 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→D is:
FIX(f)≡lub({fn(⊥):n≥0})
§ ≤ as implication
We can think of b≤a as b⟹a. That is, b has more information
than a, and hence implies a.
§ References