like that, but could have of course. The main advantage is that we become able to mix domain and set theoretic reasoning in HOL. Hence, reasoning about bottom and strict functions can often be (almost) eliminated from proofs, or deferred until the late stages of a proof.
In contrast to (2), domain theory is only present in the logic of LCF through axioms and primitive rules of inference. Therefore xed point induction is the only way to reason about recursive denitions and testing that a predicate admits induction can only be performed in ML by an incomplete syntactic check. By exploiting the semantic denitions of these concepts in domain theory, HOL-CPO does not impose such limitations. Fixed point induction can be derived as a theorem and syntactic checks for admissibility, also called inclusiveness, can be implemented, just as in LCF. But using other techniques for recursion or reasoning directly about xed points allow more theorems to be proved than with just xed point induction. Inclusive predicates not accepted by the syntactic checks can be proved to be inclusive directly from the semantic denition.
The examples will show that we can dene and reason about arbitrary recursive functions and non-termination in domain theory and about nite-valued types and to-tal (`strict') functions in set theory (higher order logic) before turning to domain theory.
The natural number example illustrates how we can mix set and domain theoretic rea-soning and thereby ease rearea-soning about strict LCF datatypes. The two other examples about recursive denitions and innite sequences respectively illustrate that we can con-duct LCF proofs by xed point incon-duction and structural incon-duction on inclusive predicates in HOL-CPO.
In the following sections these points and the most important dierences between the two systems are discussed further.
7.1.1 The Logic PP
The central dierence between LCF and HOL is in their logic parts. The logic of the HOL system is an implementation of a version of Church's higher order logic. The logic of the LCF system is an implementation of a version of Scott's Logic of Computable Functions, usually abbreviated LCF. In order to be able to distinguish the logic and the system the logic was renamed to PP, an acronym of Polymorphic Predicate -calculus.
PP is a rst order logic of domain theory it has a domain theoretic semantics. It diers from higher order logic since it is a rst order logic and since types denote cpos with bottom. The function type denotes the continuous function space. Types of the HOL logic just denote sets (cpos may be viewed as sets with structure) and functions are total functions of set theory.
Because PP is a rst order logic there is a distinction between terms and formulae and quantication is only allowed for terms. Formulae are just the usual ones of predicate calculus and terms are similar to HOL terms either an LCF term is a constant, a variable, an abstraction or a combination (application). Every such term has a type in LCF and there are both formulae and terms of type boolean. Therefore, there are also two equality tests, the computational one for terms and the logical one for formulae, written as .
In HOL there is no distinction between terms and formulae. Roughly speaking, the formulae of LCF correspond to HOL terms of type boolean. LCF terms and types can be denoted by using the extension of HOL with domain theory. Therefore, HOL-CPO can be seen as kind of shallow embedding of LCF in HOL.
Note that types of LCF correspond to pointed cpos in HOL-CPO. It is a real advantage to allow cpos without bottom since this makes it easier to view (subsets of) HOL types as cpos and eliminate reasoning about bottom. The presence of bottom in all types is very annoying in LCF (as mentioned above and demonstrated by the natural number example).
Since types of PP denote pointed cpos and all functions are continuous, it is a fact of domain theory that recursive functions can be dened by using a xed point operator.
Reasoning about recursive denitions can be conducted using xed point induction. The xed point theory of computation is provided in PP through axioms and primitive rules of inference. A constant denotes the xed point operator of domain theory due to an axiom which states it yields a xed point and due to the primitive rule of xed point induction which states it yields the least xed point. In the logic there is no domain theoretic denition of the xed point operator. Therefore, this axiom and primitive rule of inference provide the only ways for reasoning about recursive denitions. Hence, proofs that reason about recursive functions in other ways, e.g. by their xed point denition, cannot be mechanized in LCF. Besides, the concept of admissibility (inclusiveness) of predicates for induction is only present as a syntactic check performed by the rule of xed point induction. This check is not complete and examples of inclusive predicates exist that are not accepted for xed point induction in LCF. Paulson gives an example in Pa84a].
Such limitations are not present in HOL-CPO. Domain theory is embedded in HOL so we have direct access to all semantic denitions of concepts of xed point theory. In
particular, the xed point operator and inclusiveness are dened semantically and xed point induction is derived as a theorem from these denitions. Since the embedding is shallow BGH92], it allows mixing any set theoretic reasoning in HOL with domain theoretic reasoning in HOL-CPO. There is no immediate dierence between ordinary HOL terms and terms that are cpos or continuous functions. We can therefore do proofs about recursive functions by xed point induction, by the denition of the xed point operator or by any induction technique that can be derived in HOL, e.g. well-founded induction (see appendix A). Besides inclusiveness can be checked syntactically by an ML function which implements a syntactic check based on theorems derived from the denition of inclusiveness (see section 5.3). This check is very similar to the LCF one (or they are the same).
7.1.2 Extending Theories
There are quite dierent traditions of extending theories in LCF and HOL. In HOL there is a sharp distinction between purely denitional extensions and axiomatic extensions.
Denitional extensions are conservative (or safe), i.e. they always preserve consistency of the logic. Stating a new axiom may not be a conservative extension, it might introduce inconsistency (or not). In LCF there is no such distinction between axioms and denitions.
The only way to extend theories with new concepts is by introducing new axioms. First a new constant or type is given a name. Then a number of properties of the constant or type are stated as axioms. It is not possible to state axioms about a type directly, they must be stated about constants as e.g. constructor functions of a datatype or abstraction and representation functions (see below).
It is not always easy to know whether an LCF axiom is safe or not since this must be justied in domain theory. In particular, an axiom should not violate the continuity of a function. All functions are assumed to be continuous in PP since the function type denotes the continuous function space. Paulson shows how easy it is to go wrong in example 4.11 of his book Pa87]. Instead of dening recursive functions using the xed point operator an axiom can be introduced which is a recursion equation, i.e. an equation where the function constant appears on both sides of the equality sign. Such axioms are justied in domain theory since the equation follows from a property stating that the xed point operator always yields a xed point. Fixed point induction can only be used if a function is dened using the xed point operator.
As mentioned above, recursive types are also introduced by axioms. There is no recursion operator for types corresponding to the xed point operator for functions so new types cannot be dened (since there is no access to domain theory). Given a recursive domain equation of the form = F( ) where F is a continuous domain constructor the most general approach is to state the existence of abstraction and representation functions ABS : F( ) ! and REP : ! F( ) that are bijective. This approach is justied in domain theory since the isomorphismequation follows from a limitconstruction of the new domain, which is said to be a solution to the recursive domain equation (see chapter 4).
Another more direct approach works for certain recursive datatypes which can be described by a set of constructor functions, each taking a number of arguments of specied types where the function type is not used in an essential way Pa84a]. Provided such a set as an argument an ML program can introduce constants and axioms to dene a new recursive datatype in LCF. The program supports both strict, lazy and mixed (mutual)
recursive datatypes. Some of these types we can derive manually in HOL using the methods described in chapter 4. If we decided to axiomatize recursive domains as in LCF, we could probably introduce recursive domains easier than with the methods of that chapter. But axiomatizing theories does not t in well with the HOL tradition. Hence, HOL-CPO is weaker than LCF on this point concerning dening recursive domains.
In LCF, the axioms of the new datatype(s) state a number of properties about the constructor functions which are dened as constants. For instance, there is an axiom which states what the partial ordering on elements of the new type is and there is a exhaustion (or cases) axiom which states that the constructors are exhaustive, i.e. any term of that type is equal to one of the constructors for appropriate arguments of the constructor. From the axioms it is derived that the constructors are distinct and that structural induction with inclusive predicates is valid on the new type. Structural induction is derived from xed point induction.
7.1.3 Rewriting
Finally, there is a small dierence in the implementation of rewriting in the two systems.
In addition to standard HOL rewriting LCF performs conditional rewriting where it tries to simplify antecedents of conditional rewrite theorems to truth recursively. And it im-plements rewriting with local assumptions where the antecedent are used to rewrite the consequence of implicative formulae. It also does -conversion whenever possible and it employs various simplications not used in HOL, e.g. DeMorgan's Laws. Therefore proofs can be written in a very compact way in LCF. But the price to pay for powerful rewriting is of course eciency. Besides a proof which use rewriting too heavily is almost impossible to read since it has no structure. If a proof is written to re!ect the way it was invented it is more accessible for later inspection.