Comments on the Formalization

are equal we can let continuous functions be equivalence classes (sets) of HOL functions.

HOL equality will then work since it is applied to sets of functions rather than functions themselves (remember two sets are equal if they contain exactly the same elements).

However, though this is perhaps a theoretically appealing approach, it is quite awkward and dicult to work with functions as equivalence classes in practice (in particular when dening the function constructions) and it provides us with no advantages over the much simpler alternative of just working with one specic xed function in each equivalence class. Therefore this approach was chosen by requiring functions are determined by their actions.

Partial functions can also be represented by relations but this approach suers from the same disadvantage as representing functions as equivalence classes. We believe that a useful formalization should exploit features of HOL to as wide an extent as possible.

Chapter 4

Recursive Domains

Functional programming languages like Standard ML and Miranda allow the user to dene new recursive datatypes. For instance, a type of lists which are sequences of elements of the same type can be introduced by a specication of the following form

list::=Nil^jConslist

This species a recursive type operator list with two constructor functions Nil and Cons for creating elements of the type of lists. In Standard ML the type introduced will consist of strict lists, i.e. nite lists constructed using a strict version of the constructorCons. In Miranda the type will consist of lazy lists, i.e. nite and innite lists constructed using a lazy (non-strict) version of ^Cons.

Strict and lazy datatypes denote cpos. So given a specication of the form above we can introduce a cpo of strict lists and a cpo of lazy lists, or more precisely, constructors for such cpos can be introduced which take the cpo of elements as an argument. There are a number of standard techniques for this purpose which introduce the new cpos as solutions of recursive domain (isomorphism) equations. Domain equations for strict and lazy lists can be written as follows

slist =^unit (slist) llist =^void + (llist)

where unit is the cpo consisting of one element apart from the bottom element and void is the cpo consisting of no other element than the bottom element. The cpo constructions for sum and product used in the equation for strict lists are strict. The constructions in the other equations are non-strict.

As mentioned in the introduction, the three most prominent techniques for solving recursive domain equations are the categorical inverse limit construction, information systems and via universal domains like P!. Formalizing the inverse limit construction in HOL would require a complex encoding since it seems to need a \big" set (as large as the reals) closed under !-sequences (to capture innite elements). Hence, its formalization in HOL would require a substantial amount of work. Information systems and P! would be simpler to formalize since an encoding is built into their construction. Further, they seem only to need a big set closed under pairing and nite subsets.

However, due to the various encodings, formalizing these methods would extend HOL with `new worlds' dierent from the `HOL world'. For instance, the information system

81

of natural numbers would have nothing in common with the type of natural numbers in HOL. Hence, it would become impossible to exploit HOL types and tools directly. To achieve this indirectly, one would have to dene isomorphisms between the HOL world and the other worlds (to the extent to which this is possible). These would probably be painful to work with.

Our philosophy is that formalizing domain theory in HOL should support the reuse of HOL types and proof infrastructure to as large an extent as possible. In this chapter we therefore investigate more ad hoc methods to dening recursive domains. Unfortunately, this decision limits the applicability of the formalization somewhat. While on the one hand these ad hoc methods enable us to reason about certain strict and lazy recursive datatypes denoting domains, they are not strong enough to provide solutions to more (and less) dicult recursive domain equations likeE = A+E ^!E]. As a further consequence, we must accept not to be able to give denotational semantics of programming languages with recursive types, though we may be able to reason about programs and types of the languages directly by their denotations in domain theory.

In section 4.1 we show how recursive domains with nite values, i.e. cpos which cor-respond to datatypes whose elements are obtained by a nite number of applications of constructor functions, can be dened by exploiting the type denition package Me89] to introduce concrete recursive datatypes in HOL. By associating an ordering relation with a subset of a datatype we can obtain a cpo. In fact, from a recursive datatype in HOL various kinds of nite-valued recursive cpos can be obtained, including discrete cpos and strict cpos.

This approach cannot be used to dene recursive domains with innite values, i.e. cpos which correspond to datatypes whose elements are obtained by a nite or innite number of applications of constructor functions. The type denition tools cannot be used to dene innite values of a datatype it only works for well-founded types with initial models. In section 4.2, we present an approach to construct (a few) innite-valued recursive domains which focuses on the dierent kinds of elements of the domain in question. This approach has been used to construct two cpos of innite sequences of data: a cpo of lazy sequences which contains all partial and innite sequences and a cpo of lazy lists which contains in addition all nite sequences. This method works well for sequences but it becomes very complicated if we attempt to construct, for instance, a cpo of binary trees.

The reason why the type denition package can only be used to dene nite datatypes is that each new datatype is dened as a subset of a type of labeled trees which are only nite trees. In section 4.3 we present the corresponding type of (partial and) innite labeled trees in HOL more precisely, we present a predicate for a set of (partial and) innite labeled trees which could be dened as a type but we do not explicitly dene a type. This type (or predicate) consists of all partial, nite and innite labeled trees which are nitely-branching. Such trees can be represented as sets of nodes. Furthermore, with an appropriate ordering relation (a subset of) this type is a pointed cpo.

It is important to note that the only purpose of the new type (predicate) of trees is to serve as the underlying type of the new recursive cpos that we wish to introduce. The type has no value at all in the set theoretic setting for dening new HOL types, e.g. the partial elements do not make sense.

Using the labels of the labeled trees in the same way as in the type denition package, we can dene new lazy recursive domains with innite (and partial and nite) elements as a sub-cpo of the cpo of labeled trees, i.e. the underlying set is a subset of innite labeled

trees and the ordering is inherited. In order to prove a sub-cpo really is a cpo it is enough to prove it contains lubs of chains. This approach to dening cpos corresponding to lazy datatypes is described in section 4.4. These ideas about (partial and) innite labeled trees and lazy recursive domains have not been formalized in HOL. It requires more work to investigate what the best way of solving recursive domain equations would be.

In section 4.5 we discuss a few ways (not formalized) of extending the class of cpos which can be introduced by the other methods of the chapter. One approach is based on extending Gunter's work on well-founded arbitrarily-branching trees Gu93] in a way which is similar to the way we extended Melham's well-founded nitely-branching trees.

Note

Denitions of the last three sections of this chapter, more precisely section 4.3{4.5, have not been formalized in HOL (as mentioned above). In order to distinguish formalized and unformalized parts, we omit the turnstile^|- when a denition or theorem has not been formalized in HOL.