Relating Large Libraries of Mathematics

We now have some experience using our HOL/Nuprl connection. We have imported classical theories of combinatory logic and minimal logic from HOL, and used them in Nuprl to prove a constructive normalization property [10]. More recently, we have been using a large collection imported facts about basic data structures in our verification of the SCI cache coherence protocol.

There are three clear lessons to be drawn from this experience. First and foremost, sharing formal knowledge between different verification systems can be practical. Once the underlying a machinery was set up, it was far easier for us to import than to reprove the results we wanted in Nuprl. Second, the syntactic connection between HOL and Nuprl, i.e. the machinery that transports objects from HOL to Nuprl, is only part of what is needed. Also essential are mechanisms for manipulating the raw imported mathematics, in a sound way, into a form more suitable for application in Nuprl. Although the extended Nuprl semantics can interpret HOL, there are many differences between the way mathematics is represented in the two systems, and as a result, the directly imported theorems are usually of a form that makes them useless for application in Nuprl proofs. The third lesson is that massaging the theorems into the desired form is possible, and is should be largely automatable using Nuprl's theorem proving facilities.

Importation of mathematics from HOL into Nuprl is done at the theory level. An HOL theory consists of some type and individual constants, some axioms (usually definitional) constraining the constants, and a set of theorems following from the axioms (and the axioms of ancestor theories). To import a theory, one interprets the type constants with Nuprl types and the term constants with members of the appropriate types, and then proves the axioms. When this is done, the theorems can then all be accepted immediately as Nuprl theorems. Type-checking is undecidable in Nuprl, so the well-typedness of terms must be proven explicitly. This means that in addition to the axioms/definitions, it is also required to prove that each object associated with a type constant is a (non-empty) type, and that each object associated with a term constant has the type specified in HOL.

For many of the basic HOL theories, the choice of Nuprl terms used in the interpretation of HOL constants must be explicitly provided by the user. However, there is a large class we can compute automatically. HOL has an extensively-used package for making a limited form of ML-style recursive type definitions. The package takes as input a specification of the type that has a syntactic form close to ML's. The result of running the package in HOL is an extension to the set of constants and axioms of the current theory, and also new definitions and theorems for reasoning about the type. There is also a package for making inductive definitions of predicates and relations. It was not difficult to write an ML program within Nuprl to automatically compute the interpretations needed for the extensions made by these packages.

To illustrate what kind of transformations are needed on directly imported mathematics, consider a example from list theory. The following is a raw import of a HOL theorem stating that a non-empty list is a cons. Because Nuprl currently has a single flat namespace, the names of all imported constants have an ``h'' prepended to avoid conflicts with Nuprl objects. The outermost quantifier quantifiers over the type S of all (small) non-empty types (this quantifier is implicit in HOL).__{{}}

 $\forall$'a:S $\uparrow$(hall ($\lambda$l:hlist('a). 
>himplies (hnot (hnull l)) 
>(hequal (hcons (hhd l) (htl l)) l)))

Apart from the outermost quantifier, the logical connectives themselves are imported constants. The transformed, ``nuprl-friendly'' theorem generated from the above is__{{}}

 $\forall$'a:S. $\forall$l:'a List.  $\neg$mt(l) $\Rightarrow$ hd(l)::tl(l) = l.

The logical connectives in HOL are all boolean-valued functions, possibly taking functional arguments, as in the case of the quantifiers. The interpretations of these connectives use boolean logic defined within Nuprl. The boolean connectives are rewritten in the second theorem to Nuprl's normal logical connectives, which are defined using a propositions-as-types correspondence. The operator $\uparrow$ in the imported theorem coerces a boolean into a Nuprl proposition. The imported list type is defined to be Nuprl's list type, and the imported tail function is defined to be Nuprl's tail function. Note however that htl is applied, as a function, to its argument, while the Nuprl tl is a defined operator with a single operand (Nuprl also has an operator for function application, of course). We have used a notational device to suppress type arguments in the (pre-rewrite) imported theorem. Each of the imported constants in the theorem actually has at least one type argument. In the rewritten theorem, there are no hidden type arguments (the Nuprl operations are ``implicitly polymorphic'').

The most interesting point in this translation is the function for head of a list. In HOL, this is a total function on lists. When we import it into Nuprl, we must prove that the interpretation returns a value on every list, empty or not. Since hhd is polymorphic, given an arbitrary type and the empty list as an argument, it must choose some arbitrary member of the type as output. Thus we must give hhd a nonconstructive definition in Nuprl. However, we can prove that this function is the same as Nuprl's hd when the list is non-empty. This gives us a conditional rewrite which goes through for this example theorem.

In general, the rewriting of imported theorems is completely automatic, except for cases like hhd, where we may occasionally be left with a subgoal to verify the condition of some conditional rewrite. Usually such conditions are proven automatically.

One obvious limitation of the implemented connection between Nuprl and HOL is that it is one-way. It should be possible to reverse the rewriting described above, so that many Nuprl theorems could be written into a form appropriate for HOL, but there would remain the problem that the theorem's constants are interpreted, i.e. are defined as particular Nuprl terms, whereas in a counterpart in HOL the constants would be abstract, i.e. declared in a theory signature and possibly constrained by axioms. Although the constructive interpretation of HOL mathematics is ultimately useful in Nuprl, there is no fundamental reason why much of the mathematics built in Nuprl on top of imported math could not be done at the same level of abstraction as in HOL, delaying interpretation until necessary.

We plan to expand the Nuprl/HOL prototype link in several ways. First, we will use the mechanisms described elsewhere in the proposal for structuring and organizing Nuprl libraries to account for HOL's notion of theory. Building on this, we will make the connection 2-way, allowing certain chunks of mathematics developed in Nuprl to be exported to HOL. Also, there are a number of practical problems that need to be addressed. These include: general robustness and ease of use; incrementally exchanging growing theories; system support to help a user ensure that their mathematics is exportable, when desired; more automation for determining interpretations of constants from HOL theories within Nuprl; and more automation and organization for specifying the correspondences used in rewriting, e.g., imported HOL facts into their Nuprl-friendly form.

We see no fundamental problem to implementing a connection between PVS and Nuprl along the Nuprl/HOL lines discussed above. Other provers, for example Coq [7], should be possible too. This gives the possibility of constructing shared libraries of basic mathematics. Some libraries, like list theory, will be basic enough that they can be shared between most systems that can be interpreted in the LPE. Of course, this will often require rewriting to put the theorems in the form most appropriate for the particular prover. Other libraries may rely on features, such as higher-order logic, present in only some systems.

One hindrance to this idea of sharing mathematics is that currently, most theories are simply not designed for reuse. Users tend to do demand-driven development of basic theories, only doing enough to complete the proof of the ultimate theorem of interest, and investing little thought in abstractions that would make the theories more reusable. This is a problem not unique to theorem-proving, of course, and the solution should be mostly a matter of motivation and will.