§ 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
§ Posets, (least) upper bounds
- A partial order (P,≤) is a set equipped with a reflexive, transitive, relation ≤ such that x≤y and y≤x implies x=y.
- A subset D⊆P is said to have an upper bound uD∈P iff for all d∈D, it is true that d≤uD.
- An upper bound is essentially a cone over the subset D in the category P.
- A subset D⊆P has a least upper bound lD iff (1) lD is an upper bound of D, and (2) for every upper bound uD, it is true that lD≤uD
- Least upper bounds are unique, since they are essentially limits of the set D when D is taken as a thin category
§ Directed Sets
- A subset D⊆P is said to be directed iff for every finite subset S⊆D, S has a upper bound dS in D. That is, the set D 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 D has all of its limit points.
- Categorically, this means that D⊆P taken as a subcategory of P 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 D 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 D? why not external upper bounds in P?
- QUESTION: why only upper bounds in D? why not least upper bounds in D?
- ANSWER: I think the point is that as long as we ask for upper bounds, we can pushforward via a function f, 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 D⊆P has a least upper bound in P.
- Compare to chain complete,
CCPO
, where every chain has a LUB. - QUESTION: why not postulate that the least upper bound must be in D?
- In a DCPO, for a directed set D, denote the upper bound by ∪D.
§ Monotonicity and Continuity
- A function f:P→Q between posets is said to be monotone iff p≤p′ implies that f(p)≤f(p′).
- A function f:P→Q is continuous, iff for every directed set D⊆P, it is true that f(∪D)=∪f(D).
- This has the subtle claim that the image of a directed set is directed.
§ 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