§ Crash course on DCPO: formalizing lambda calculus
In lambda calculus, we often see functions of the form . 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 of values
which contains its own function space: . This
seems to ask for a set whose cardinality is such that , which is
only possible if , ie 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
- We can see that the cardinality of is different from the cardinality of the space of functions over it, .
- However, "the set of all functions" isn't really something mathematicians consider. One would most likely consider "the set of all continuous functions" .
- 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 , you can give me a continuous function which I can Cauchy-complete, to get a function .
- Now, cardinality considerations tell us that:
- We've won! We have a space whose space of continuous functions is isomorphic to .
- 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 is a set equipped with a reflexive, transitive, relation such that and implies .
- A subset is said to have an upper bound iff for all , it is true that .
- An upper bound is essentially a cone over the subset in the category .
- A subset has a least upper bound iff (1) is an upper bound of , and (2) for every upper bound , it is true that
- Least upper bounds are unique, since they are essentially limits of the set when is taken as a thin category
§ Directed Sets
- A subset is said to be directed iff for every finite subset , has a upper bound in . That is, the set 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 has all of its limit points.
- Categorically, this means that taken as a subcategory of 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 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 ? why not external upper bounds in ?
- QUESTION: why only upper bounds in ? why not least upper bounds in ?
- ANSWER: I think the point is that as long as we ask for upper bounds, we can pushforward via a function , since the image of a directed set will be directed.
§ Directed Complete Partial Order (
- A poset is said to be directed complete iff every directed set has a least upper bound in .
- Compare to chain complete,
CCPO, where every chain has a LUB.
- QUESTION: why not postulate that the least upper bound must be in ?
- In a DCPO, for a directed set , denote the upper bound by .
§ Monotonicity and Continuity
- A function between posets is said to be monotone iff implies that .
- A function is continuous, iff for every directed set , it is true that .
- This has the subtle claim that the image of a directed set is directed.
§ Monotone map
- A function from to is said to be monotone if .
- 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:
This does not preserve least-upper-bounds. Consider the sequence of elements:
The union of all is .
Each of these sets is finite.
Hence , and so on. Therefore:
§ 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 is:
§ as implication
We can think of as . That is, has more information
than , and hence implies .