|- !D.
Seq_of_FUN =
(\sf :: Dom(cf(cf(D,D),cf(D,seq D))).
\f :: Dom(cf(D,D)). \x :: Dom D. Cons_seq x(sf f(f x)))
|- !D. Seq_of = Fix Seq_of_FUN
Both are dened using new constructor definition. The continuity theorems re-turned by this program are stated as follows
|- !D.
cpo D ==>
Seq_of_FUN ins
(cf(cf(cf(D,D),cf(D,seq D)),cf(cf(D,D),cf(D,seq D))))
|- !D. cpo D ==> Seq_of ins (cf(cf(D,D),cf(D,seq D)))
It should be apparent from the xed point denition of Seq of that it always computes an innite sequence.
We can now prove the following statement about Seq of and Maps
|- !D f.
cpo D ==>
f ins (cf(D,D)) ==>
(!x. x ins D ==> (Seq_of f(f x) = Maps f(Seq_of f x)))
Informally, the two sequences are equal since they are both equal to a term corresponding to f x f(f x) :::] . The proof of the theorem is conducted by xed point induction on both occurrences of Seq of. But rst the two rst antecedents are stripped o and a case split is performed on whether D is empty or not. If it is then an induction is not necessary since "x ins D" must be false. Otherwise, the remaining predicate is proved to be inclusive (as a function of a variable replacing Seq of ) and xed point induction is conducted. Examples of the use of xed point induction has been given above. We shall not consider the details of this induction proof here.
Again the proofs in our formalization and LCF are based on the same overall idea but tend to be longer in HOL since we do the simplications explicitly whereas LCF rewriting handles many situations. As mentioned above this probably makes LCF rewriting ine-cient at least compared to HOL rewriting but our simplications are quite ineine-cient too, since they do more than just rewriting e.g. they also do type checking.
reasoning about strict LCF datatypes and functions. The extension is more useful than
`pure' HOL for reasoning about innite-valued types and arbitrary recursive functions and more useful than LCF for reasoning about nite-valued types and strict functions.
In a way, HOL-CPO can be seen as an embedding of the LCF system in HOL which is performed in such a way that the benets of the HOL world are not lost.
The natural number example illustrates how we can mix set and domain theoretic rea-soning and thereby ease rearea-soning about nite-valued LCF types and strict functions. We avoid denedness assumptions (complicating statements and proofs in LCF) and natural number inductions involving bottom completely. Another example illustrating this point is presented in chapter 8 (the unication algorithm).
The example on a xed point denition shows that we can dene an arbitrary recursive function in HOL-CPO and reason about it using xed point induction. This development follows the development in LCF closely and would not be easy in pure HOL.
Finally, the example on lazy sequences gives a denition of an innite sequence con-structor functional as a xed point and illustrates that we can conduct LCF proofs by xed point induction and structural induction on lazy recursive domains in HOL-CPO.
Again we follow the LCF denitions and proofs closely since pure HOL does not support this kind of reasoning directly.
Some disadvantages of the embedding of domain theory in HOL have also been men-tioned. One main problem is that it is time-consuming and not at all straightforward to introduce new recursive domains (see chapter 4). Another problem is that construc-tors must be parameterized by the domains on which they work. This inconvenience is handled by the interface in most cases but the problem also makes proofs inconvenient since type checking must be performed quite often. LCF rewriting uses-conversion after function denitions have been expanded to handle this. Rewriting is fairly powerful in LCF, providing conditional rewriting and rewriting with local assumptions, and it han-dles many situations in a compact way. Therefore LCF `induction then rewriting' proofs about innite-valued types and lazy evaluation tend to be longer but just as simple in HOL where dierent tactics are used for each specic task.
HOL-CPO is a semantic embedding of domain theory in a powerful theorem prover.
It was an important goal of this embedding that there should be a direct correspondence between elements of domains and elements of HOL types. This allows us to exploit the types and tools of HOL directly and hence, to benet from mixing domain and set theoretic reasoning as discussed above. The fact that we use predomains, i.e. cpos which do not necessarily have a bottom, also supports this.
A semantic embedding does not always have this property. The formalization of P! in Pe93] builds a separate P! world inside HOL so there is no direct relationship between for instance natural numbers in the P! model and in the HOL system. The same thing would be true about a HOL formalization of information systems Wi93].
Chapter 8
Verifying the Unication Algorithm
The problem of nding a common instance of two expressions is called unication. The unication algorithm generates a substitution to yield this instance, and returns a failure if a common instance does not exist. The algorithm has played a central role in logic programming and theorem proving after it was used by Robinson in 1965 in his resolution principle for automatic theorem proving Ro65].
Manna and Waldinger (MW) synthesized the unication algorithm by hand using their deductive tableau system MW81]. Their informal presentation of the proof was unusually complete providing all lemmas (without proof) and the entire main body of the proof which covered morethan 15 pages (the paper itself covered more than 40 pages). The constructive proof from which they extract the algorithm relies on a substantial theory of expressions and substitutions and employs the very general principle of well-founded induction for the proof of correctness. They work in an ordinary untyped rst-order logic where variables range over sets and functions are total.
Paulson translated MW's proof to a mechanical proof in LCF Pa85]. Paulson's proof follows their proof closely. However, he did not deduce the algorithm from the proof as they did he stated the algorithm rst and then proved it was correct. Mechanizing the proof in LCF was rather dicult, both due to the logic, the limited range of available induction strategies and the lack of proper proof infrastructure.
Coen did yet another version of the proof in his implementation of CCL (Classical Computational Logic) in the Isabelle theorem prover Co92]. His logic supports the proof of correctness well, in particular, because it provides well-founded induction, which is needed for the termination proof of the algorithm.
The underlying logic of the LCF system is entirely dierent from the logic used by MW since variables range over domains rather then sets and functions may be partial.
The consequence of this was that denedness assertions of the form t ? appeared everywhere, complicating both statements and proofs considerably, and it was necessary again and again to use and prove the totality of functions which were obviously total.
These problems arose since all datatypes and functions were strict (cf. section 7.2 on the natural numbers).
Further, the well-founded induction used by MW was not used in the LCF proof it is not clear whether or not it is possible to derive well-founded induction in LCF. Instead this was inconveniently translated into two nested structural inductions on the natural numbers and terms, respectively. The algorithm contains an unusual and non-trivial recursion so a simple induction argument was not enough to prove termination.
185
Finally, the LCF systemcontained very littleproof infrastructure when Paulson started this project. The present tools to dene recursive datatypes and to perform proof by structural induction (see section 7.1) were developed by Paulson as part of the project.
In this chapter we describe an implementation of MW's proof in HOL-CPO which is based directly on Paulson's proof in LCF1. The HOL system seemed to provide a much more appropriate framework for implementing the proof. Its underlying logic is based on set theory and total functions and well-founded induction is available due to the development presented in Ag91, Ag92]. It also provides substantial theories of sets and lists, among others, which may be useful to formalize the various datatypes in the proof.
It supports the denition of new abstract recursive datatypes and primitive recursive functions and it allows proof by structural induction. However, it is not easy to dene the unication algorithm directly in pure HOL, since it is not primitive recursive. The unusual recursion in the algorithm makes a proof of termination non-trivial. Here, domain theory appears useful. We can dene the recursive algorithm as a xed point of an appropriate functional and prove termination afterwards, using well-founded induction.
Hence, combining the theory of well-founded sets and the formalization of domain theory in HOL, we become able to extend the methods for dening recursive functions in HOL to allow dening functions by well-founded induction (see also the Ackermann example of chapter 2).
In the following sections we describe the implementation of the correctness proof of the unication algorithm in HOL-CPO. The rst three sections do not use any domain theory at all!