where EVERY is used to state that the predicate Is infinite tree holds for all elements of a list of subtrees.
Assuming we have a cpo of labels we know innite tree with labels in that cpo is also a cpo. We would like a continuous constructor NodeI for trees behaving like the node constructor above. So, NodeI should be in the following continuous function space
NodeI D ins cf(D,cf(list(itree D),itree D))
and it can be dened as the lambda abstracted version of node .
NodeI D = lambda D(\a. lambda(list(itree D))(\trl. node a trl))
Note that NodeI is parameterized by the domain D . The list cpo is simply a subset of the HOL list type with the ordering that relates only lists of equal length whose elements are related (see section 4.1).
subtree tr tr' = ?p. !p' l. (p',l) IN tr ==> (p++p',l) IN tr'
So a tree tr is a subtree of a tree tr' if the nodes of tr are present in tr' at the same position (as in tr) relative to the root of tr (in tr').
4.4.1 Example: Lazy Lists
Lazy lists can be described by the following type specication
llist = nil | cons * llist
So apart from the bottom list, lazy lists have two constructors: one for the empty list and one for adding an element to a list.
We can introduce a type predicate for lazy lists as a subset of the type predicate for innite trees. More precisely, the representing `type' of lazy lists is
Is_infinite_tree: ((one + *)node -> bool) -> bool
where the labels have type ":one + *". The label type is constructed from the type specication by taking the rst component of the sum to be the type ":one" because
nil takes no arguments and taking the second component to be":*"because the second constructor takes elements of this existing type as arguments.
The bottom lazy list is simply the bottom node of innite trees, i.e. Bt node. We can dene predicates to identify which trees correspond to the empty list nil and the list constructor cons as follows
Is_nil v trl = ?a. (v = LBL(INL a)) /\ (LENGTH trl = 0) Is_cons v trl = ?a. (v = LBL(INR a)) /\ (LENGTH trl = 1)
A node of the representing type of trees can be interpreted as the empty list if it has no subtrees (nil takes no lists as arguments) and its label is in the left component of the sum type. A node can be interpreted as a non-empty list if it has precisely one subtree (since cons takes one lazy list as an argument) and its label is in the right component of the sum type (corresponding to the rst element of the resulting list).
The constructor predicates are used to dene precisely which subset of innite trees corresponds to lazy list in the following way
Is_llist ll =
Is_infinite_tree ll /\
(ll = Bt_node) \/
(!v trl. (node v trl) subtree ll ==> Is_nil v trl \/ Is_cons v trl)
In order to interpret this denition recall that innite trees satisfy the exhaustion axiom (constructors are onto). That is, either a tree is equal to the bottom node or there exist a label and a list of subtrees, each of which is an innite tree, such that it is equal to the node with this label and list of subtrees. The second disjunct above states that for any subtree of a tree the root node must be the empty list or a non-empty list. Thus all nodes of a tree representing a lazy list is either a partial node, an empty list node with no subtrees or a non-empty list node with precisely one subtree (the root of which is again a node of the tree and so on).
Since we identify rather than actually dene types in HOL we avoid type abstraction and representation functions in terms. If we wish we can introduce a type of lazy lists without problems. It is less practical to dene a type of innite trees because we use the set representation again and again.
We can now dene the cpo of lazy lists of elements of some cpo as a sub-cpo of a certain cpo of innite trees
llist D =
{ll | Is_llist ll /\ ll ins (itree(sum(One,D))}, itree_rel (sum(One,D))
where One is the discrete universal cpo "discrete UNIV" based on the type ":one". Note that the innite trees used here are labeled by elements of a sum cpo the underlying type of which corresponds to the label type used above to identify the type of lazy lists.
The above denition of a type (and domain) of lazy lists guarantees that all nodes of a non-bottom tree representing a non-bottom lazy list is a nil node or a cons node.
These constructors are dened by
nil = node(LBL(INL one))]
cons h t = node(LBL(INR h))t]
The constant cons is not determined but a determined and hence continuous version of
cons is obtained easily as follows
ConsI D = lambda D (\a.
lambda(llist D)
(\ll. NodeI(sum(One,D))(LabelI(sum(One,D))(InrI(One,D)a))ll]))
where we have exploited that NodeI has been proved once and forall to be a continuous (determined) version of node used to dene cons (this saves proof commitments). The constant LabelI is a continuous version of the constant LBL (see page 99).
We can prove the structural induction theorem for inclusive properties of lazy lists in exactly the same way as for lazy lists in section 4.4.1 using the copying function.
4.4.2 The Method in General
We will now describe how the denotations of lazy datatypes in general can be dened using the type (predicate) and cpo of innite labeled trees. The method is exactly the same as in the type denition package Me89], i.e. we choose the labels and number of subtrees of innite trees in the same way as the labels and number of subtrees of nite labeled trees are chosen there.
In general a type specication takes the following form
rty ::= C1 ty11 ... ty1k1 | . . . | Cm tym1 ... tymkm
For the i'th constructor let pi stand for the number of existing types in the specication and let qi stand for the number of occurrences of rty. Thus, ki is equal to the sum of
pi and qi . The existing types may be polymorphic types or not. The type predicate and
the cpo constructor corresponding to the specication will depend on the polymorphic types.
The recursive type (predicate) corresponding to this type specication can be intro-duced as a subset of innite trees. The representing `type' has the following form
Is_infinite_tree: (((ty#...#ty)+...+(ty#...#ty))node -> bool) -> bool
There are m elements of the sum, one for each constructor. The products of the sum consist of p1 , :::, pm components. These components are the existing types in the type specication of each constructor. Thus, the name ty occuring in the label type is used to indicate `some type' (in order to save indices). Dierent occurrence of ty may correspond to dierent types.
For each constructor we dene a predicate to specify which trees represent values constructed by that constructor. The predicate for the i'th constructor is dened as follows
Is_Ci v trl =
?x1...xpi.
(v = LBL(INR(...(INR(INL(x1,...,xpi)))))) /\ (LENGTH trl = qi)
There are i;1 occurrences of INR. Ifi is equal to m then the INL is omitted.
The recursive type corresponding to the specication of rty can now be dened as the following subset of innite trees
Is_rty tr =
Is_infinite_tree tr /\
(tr = Bt_node) \/
(!v trl.
(node v trl) IN tr ==> Is_C1 v trl \/ . . . \/ Is_Cm v trl)
Keep the restrictions imposed on trees by the predicate Is infinite tree in mind when interpreting the second disjunct of this denition (see the example of section 4.4.1). It states that all nodes of a tree must correspond to a node which has been constructed using one of the constructors.
Some of the existing types of the type specication may be polymorphic types, in-volving say type variables 1, :::, n. For each type variable the cpo constructor for the specication becomes parameterized by a cpo variable with the type variable as the underlying type. In order to dene the cpo constructor we must know the cpos corre-sponding to the types of the specication. The cpo of lazy elements of type Is rty can be dened as follows
rty(D1,...,Dn) =
ftr | Is_rty tr /\ tr ins (itree(sum(prod(...),sum(...))))g, itree_rel (sum(prod(...),sum(...)))
where the type of each variable Di is ":(i)cpo", which is a piece of syntactic sugar for the type ":(i -> bool) # (i -> i -> bool)" (introduced in chapter 3). The sum cpo of product cpos which is an argument of itree (and itree rel above is the cpo of labels. The underlying type of this cpo was described above. Typically, sum types, product types and function types in the type of labels are replaced by the corresponding
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).