Conclusion

where^Mapsis the mapping functional dened in section 2.5.1 above. From the xed point property we derive the following recursion equations:

`nats=Cons seq0(Maps^SUCnats)

`8n: ^fromn =^{Cons seq}n(^from(^SUCn))

Hence, it does not seem unreasonable to attempt to prove the equality: ^nats = ^from0.

The proof is by co-induction with the bisimulation

`bisim seq^seqNat(ss⁰:⁹n: s =^{Maps iter}n^{nats^}s⁰=fromn)

where ^{Maps iter}ns iterates the mapping functional n times over a sequence s of natural numbers:

`(^{Maps iter}0 = (x^2seqNat: x))^{^}

(⁸n: ^{Maps iter}(^SUCn) = (x^2seqNat: ^{Maps iter}n(^MapsSUCx)))

To prove the suggested relation is a bisimulation, the second disjunct of the denition of bisimulation is established by choosing x to be n, s to be ^{Maps iter}(^SUCn)^nats and s⁰ to be from(^SUCn). Note that the continuity of ^{Maps iter} does not follow from the notation of typable terms immediately since it takes its rst argument without the use of the dependent lambda abstraction. However, the continuity is easily established sinceNat is a discrete universal cpo. Another consequence of using a primitive recursive denition of ^{Maps iter} is that we must use structural induction to derive the recursion equations:

`(⁸x:Maps iter0x = x)^{^}

(⁸nx:^{Maps iter}(^SUCn)x =^MapsSUC(Maps iternx))

With a xed point denition these could be derived by appealing to the xed point property. Note that the cpo of sequences of elements in a universal cpo is itself a universal cpo (i.e. it contains all elements of the underlying type).

Once the bisimulation has been invented the proof is straightforward. The two se-quences are trivially related by the bisimulation since their rst elements are the same.

It should be clear to the reader that HOL-CPO extends HOL with a number of useful concepts and techniques. In HOL-CPO one may reason about partial functions and nontermination and more general recursive (computable) functions may be dened, using the xed point operator. Fixed point dened recursive functions must in general be (potentially) partial functions in order to allow taking the least xed point. But some recursive functions can be proved to be total, for instance, by well-founded induction, and this allows the derivation of recursion equations for pure HOL recursive functions. In this way, HOL-CPO supports recursive function denitions by well-founded induction. This point was illustrated by the example on Ackermann's function (see section 2.3.2).

One of the weaknesses of the formalization is the need for the dependent lambda ab-straction and cpo parameters on certain function constructions. This makes the syntax of functions inconvenient, though an interface can hide much of this inconvenience. Further, it complicates proofs since arguments of functions must be type checked before dependent lambda abstractions can be reduced. Again, this has been automated to some degree.

In the following chapters the formalization and the associated tools are presented in more details than here. We shall switch to real HOL syntax and show real HOL sessions to illustrate the use of HOL-CPO. Chapter 6 and chapter 7 provide fairly small and simple examples, some of which have been presented here too (some examples are only presented in this chapter). A larger example showing the proof of correctness of a unication algorithm is presented in chapter 8. For a more full discussion on HOL-CPO, the reader should consult the conclusion chapter 9.

Chapter 3

Basic Concepts of Domain Theory

Most computer scientists are familiar with the basic concepts of domain theory, such as complete partial orders (cpos), continuous functions and least xed points. In denota-tional semantics, types of data are modeled as cpos and programs as continuous functions between cpos. Recursion is handled by taking least xed points of continuous functionals, nontermination using a so-called bottom or undened element of cpos. Good introduc-tions on domain theory are provided in the textbooks by Winskel Wi93], Schmidt Sc86]

and Gunter Gu92].

In this chapter we provide an overview of a formalization of basic concepts of domain theory in HOL, based mainly on the book by Winskel. The notions of cpos and continuous functions are introduced as semantic constants in HOL stating a number of conditions that terms must satisfy in order to be cpos and continuous functions. Cpos are represented by HOL pairs of sets and ordering relations and continuous functions are represented as HOL functions.

It is important to note that there is a direct correspondence between elements of cpos and elements of HOL types: the underlying set of a cpo is a subset of a HOL type. As discussed in the examples (see chapter 6{8), this allows us to exploit the rich collection of theories and tools provided with the HOL system and we become able to mix domain and set theoretic reasoning in HOL. Thereby, the often quite painful reasoning involving bottom (as in LCF) can be almost eliminated and deferred until the late stages of a proof.

The semantic conditions on cpos and continuous functions can be proved to hold of terms manually in the HOL system. However, such ad hoc proofs quickly become tedious and complicated so it is desirable to have standard ways of writing terms which guarantee that they satisfy the semantic conditions. We therefore dene a number of constructions on cpos and continuous functions below, which provide syntactic notations for writing cpos and continuous functions. Proof functions have been implemented in ML to support these notations in the sense that they automatically prove the desired properties of terms which t within the notations (see chapter 5). As one example of a construction on cpos, we can mention that the continuous functions between two cpo D¹ and D² constitute a cpo with the pointwise ordering, usually written D^{1 !} D²]. This cpo is called the continuous function space or the cpo of continuous functions.

Some might think that the set part of a cpo set and relation pair could be avoided by representing it directly as a HOL type instead of as a subset of a HOL type. This is not the case. The need for the set component arises since we wish to dene the continuous function space construction on cpos. The underlying set of continuous functions cannot

49

be the HOL type of functions itself, because in general this type may contain functions which are not continuous. Furthermore, the desired type cannot be dened in HOL since it is a dependent subtype of the HOL function type, dependent on free term variables corresponding to cpos (see section 3.11). Hence, the set component of the set relation pair approach described here is used to represent this dependent type. This complicates the formalization somewhat, since many problems from dependent type theory are introduced.

E.g. terms must be `type checked' manually, i.e. we must prove manually which cpos terms belong to. This is not handled by HOL type checkingalone. Furthermore, extra conditions must be introduced to ensure that functions map subsets of types to subsets of types and behave properly outside cpo subsets|this last condition is called determinedness.

In order to ensure the functions we write are determined, a kind of dependent lambda abstraction is introduced. Thus we cannot use the built-in lambda abstraction and -conversion. A consequence is that all function constructors become parameterized by the domains on which they work more precisely, they become parameterized by the cpo variables of their domain cpos. In addition, arguments of functions must be type checked in order to ensure they belong to the right domains. Fortunately, the disadvantages of this can be minimized by an interface consisting of a parser and a pretty-printer, which hides the cpo parameters when they are not `necessary', and by a proof function called the type checker which can prove in certain cases which cpo a term belongs to from the way in which it is constructed syntactically. The interface and type checker are described in chapter 5.

Note

The presentation below is quite detailed, listing a lot of denitions and theorems of do-main theory (without proofs). After reading the overview in section 2.1 of the previous chapter, it may be enough to skim this chapter. However, the discussion of section 3.11 is recommended.