sum, product and function space constructions on cpos, respectively. The construction introduced by this denition can be proved to be a construction on pointed cpos, by proving that it yields a sub-cpo of the pointed cpo of innite trees for all arguments.
The constructors of the new recursive `type' are dened using the tree constructor
node and the injections INL and INR as follows
Ci xik1 ... xiki =
node(LBL(INR(...(INR(INL(xiyi1,...,xiyipi))))))xizi1...xiziqi]
where xiyij corresponds to arguments which according to the type specication have an existing type. Conversely, xizij corresponds to arguments which according to the type specication are recursive. A continuous version of each constructor can be obtained using the dependent lambda abstraction or by a denition corresponding to the one above where continuous functions are used instead of the non-determined ones (see the example of section 4.4.1).
4.5.1 Broad Trees
First a type predicate for unlabeled trees is dened as a subset of sets of lists:
Is_unlabeled_tree tr = ]IN tr /\ (!p p'. (p++p') IN tr ==> p IN tr)
So, an unlabeled tree is represented by a set of nodes of type":(*)list -> bool"where each node is a path from the root to that node. A path is a list of branch indices.
A labeling of an unlabeled tree assigns labels to the nodes of the tree. We let labelings be partial functions of type ":(*)list -> (**)upty" where the type specication of
upty is
upty = undef | up *
such that the nodes for which they are dened (not equal to undef) correspond to unlabeled trees:
Is_labeling l = Is_unlabeled_tree(part_fun_domain l)
It is straightforward to dene the constant part fun domain:
part_fun_domain l = {p | ~(l p = undef)}
Note that the type specication of the upty is similar to the lty type operator dened in section 3.6.4 and the label type operator dened in section 4.4. We prefer dierent names since they are used to do slightly dierent things.
The predicate Is labeling denes the broad trees in the work by Gunter Gu93]. A subset of the type of broad trees correspond to well-founded arbitrarily branching trees called `bonsai' in Gu93] which are used to represent a generalization of Melham's types.
However, we wish to be able to distinguish partial nodes from labeled nodes. Therefore our broad trees will be a subset of an instance of labelings, dened as follows
Is_broad_tree (l:(*)list -> ((**)label)upty) = Is_labeling l /\
(!p. (l p = up NOLBL) ==> !p'. ~(p' = ]) ==> (l(p++p') = undef))
where the labels of trees have type ":(**)label", not ":**"as in Gunter's broad trees.
The second conjunct makes sure that partial nodes do not have subtrees. We will use the following syntactic sugar for the `type' of broad trees
(*,**)brotr == (*)list -> ((**)label)upty
The name brotr abbreviates `broad tree'.
Next, we dene the ordering on broad trees which must enable us to dene a cpo construction on broad trees:
brotr_rel D l l' =
(!p. (l p = up NOLBL) ==> (?x. l p = up x)) /\
(!p v.
(l p = up(LBL v)) ==> (?v'. rel D v v' /\ (l' p = up(LBL v'))) /\
(!p.
p IN part_fun_domain l' /\ ~p IN part_fun_domain l ==>
(?p' p''.
(p = p'++p'') /\ p' IN part_fun_domain l /\ (l p' = NOLBL)))
Hence, two broad trees l and l' are related if, and only if, a partial node of l is also present as a node (partial or not) in l', a labeled node of l is also a labeled node of
l' such that the labels are related, and a node in l' which is not a node in l belongs to a subtree of l' replacing a partial node of l.
The construction on pointed cpos of broad trees is dened as follows
brotr D =
{l | Is_broad_tree l /\ (brotr_label_set l) subset D}, brotr_rel D
where
brotr_label_set l = {v | ?p. l p = up(LBL v)}
Note that the cpo parameter of brotr corresponds to the cpo of labels whereas elements of the branching type ":*" are not required to be elements of a cpo. E.g. we will not take least upper bounds over the way in which trees are branching. To justify that brotr does yield a construction on cpos, here is the way that lubs of chains of broad trees are constructed:
brotr_lub D X = (\p.
(?n. ?v. X n p = up(LBL v)) =>
let n = (@n. ?v. X n p = up(LBL v)) in
up(LBL(lub(cset(\m. @v. csuffix(X,n)m = up(LBL v)),D))) | (?n. X n p = up NOLBL) => up NOLBL | undef)
The denition constructs a broad tree, i.e. a function from paths to `up-lifted' labels. For a xed path argument of the construction, the rst condition tests whether there is an tree in the chain such that the path corresponds to a labeled node in that tree. If this is the case then the rest of the trees in the chain also has a labeled node at the same position. Hence, the lub construction at this position must be the lub of these labels.
Otherwise, there might be a point from which the node corresponding to the path is an unlabeled node. In this case the lub construction must be an unlabeled node at this point.
Otherwise, the lub construction yields undened because no trees of the chain has a node at the position specied by the path.
It is straightforward to dene constructors for broad trees:
Bt_brotr = \p. ((p = ]) => up NOLBL | undef)
node_brotr (a:**) (subtrees:*->((*,**)brotr)upty) =
\p.
(p = ]) => up(LBL a) |
(subtrees (HD p) = undef) => undef | lower(subtrees(HD p))(TL p)
where lower is dened by
lower(up a) = a
Note that subtrees of a node are represented as partial functions such that the number of subtrees may vary at each node of a tree (due to undef). Continuous versions of the constructors can be dened as in the previous sections.
So, we have dened a type predicate for broad trees and an ordering relation which makes (a subset of) broad trees into a cpo. The next step is to show how new recursive datatypes can be dened as subsets of broad trees and how the corresponding cpo can be dened as sub-cpos of the cpo of broad trees. Then the constructors for the new type, and continuous constructors for the cpo, must be dened.
Here, we shall only commenton how to dene a type predicate for new recursive types, given a type specication of the following form
rty ::= C1 ty11 ... ty1k1 | . . . | Cm tym1 ... tymkm
where each tyij is either an existing logical type (not containing rty) or of the form
":ty -> rty" for some existing type expression ty. The method described in the pre-vious section corresponds to the case where ty is the type one. Further generalization is discussed in Gu93].
A new type can be represented as a subset of broad tree with a certain branching type and a certain labeling type. Both of these are a sum type with a component for each constructor of the specication. The contribution of the constructor case Ci tyi1 ...
tyiki to the branching type is (again) a sum of existing types etyij where tyij =
etyij -> rty, or one if none such exists. The contribution to the labeling type is the product of each existing type and one if there are no existing types. This is exactly the same approach to constructing the branching and labeling types as in Gu93] which can be conferred for further details.
Chapter 5
The HOL-CPO System
Up to this point we have considered the formalization of domain theoretic concepts in HOL and not so much using this formalization. We have presented the basic denitions as well as constructions on cpos and continuous functions which give ways of writing terms that are guaranteed to be cpos and continuous functions. We have also shown how certain recursive domains can be introduced, e.g. strict and lazy lists. However, it is not practical to use the formalization as presented above directly. One must prove all the time that terms are cpos (or pointed cpos), continuous functions and inclusive predicates, e.g.
each time the xed point property of Fix is used (see section 3.8) or each time the xed point induction theorem is used (see section 3.9). In particular, proofs of continuity may require a substantial amount of work when function denitions involve nested lambda abstractions and are longer than a couple of lines. Besides, function constructions are tedious and dicult to read and write since they are parameterized by the cpo variables of the domains on which they work.
So, in order to make the formalization useful for reasoning about functional programs in practice, there are at least two things we should do:
develop an interface which supports a less tedious syntax for functions, and
provide syntactic-based proof functions to prove automatically that certain terms are cpos, continuous functions and inclusive predicates.
Actually, it is advantageous to treat proofs of continuity facts as a special case of the more general problem of proving that a term belongs to some cpo. We can solve this problem in many cases with a syntactic-based proof function for constructing the cpo of a term. This function is called the type checker terms that are elements of a cpo are called cpo-typable terms, or just typable terms. The syntactic-based proof functions for cpos and inclusive predicates are called the cpo prover and the inclusive prover, respectively. The notations supported by the interface and these syntactic-based proof tools are not xed, they can be extended by declaring new constructor terms. On top of the syntactic-based proof tools and the declaration tools a number of derived denition tools have been implemented for introducing cpos and arbitrary terms in cpos as abbreviations of terms which t within the syntactic notations.
The result of these developments is an integrated system, called HOL-CPO, where domain theory seems almost built-in to the user. Basic proof tools are applied behind the scenes so in most cases the user does not have to worry too much about proving
111
domain theoretic concepts in order to employ the formalization. (However, the tools are prototypes and are therefore not as optimized and powerful as they could be.)