§ 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
- Given a partial order . assume we have a subset . A least upper bound of is an element that is the smallest element in which is larger than every element in .
- A subset of is called as a chain if its elements can be put into order. That is, there is a labelling of elements of into such that .
- 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 .
- TODO: example of ccpo that is not a lattice
§ 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 .