Details of relating type theories

In order to allow sharing of mathematics between Nuprl and systems like HOL and PVS [25] that use classical logic, a fundamental extension to Nuprl was required. Of course, it is trivially possible in principle to embed any one of these systems in another by, for example, formalizing the proof theory, but we were after a practical connection. For example, if some new theorems about the integers are proven in HOL, we want to automatically import them as theorems about the Nuprl integers. More generally, we want to interpret HOL in Nuprl, using specific objects of interest for parts of the interpretation.

Because Nuprl has an expressive and flexible type system, it is straightforward to naturally interpret the type systems of classical type theories such as HOL and PVS. In particular, the function type is interpreted as Nuprl's function type. The difficulty is in dealing with the classical nature of the theories, which is captured in the ``epsilon'' operator, which given a type A and a predicate P over A chooses some member of A satisfying P (an arbitrary value if no such value exists).

Nuprl, with the original semantics, is a logic of computable functions. All members of a function type $A\rightarrow B$ must be computable. The semantics assigns to $A\rightarrow B$ a set of untyped functional programs which have the right input-output behaviour. The behavior of programs is given operationally. Since the epsilon operator can be used to build non-computable functions, to interpret it appropriately we need to augment the Nuprl semantics.

This was the primary motivation for the work in [15] and [17]. This work shows how to combine untyped functional programming languages with objects from conventional set theory such as functions-as-graphs, equivalence classes, and types as sets. Programs are tightly integrated with the set-theoretic objects. For example, function types contain both programs and set-theoretic graphs of functions. The semantic explanation is an extension of the original operational semantics. The language of programs is extended with constants from a set theoretic universe, and ``evaluation'' rules are added to the semantics to explain, for example, how to apply a graph of a function to an arbitrary program.

The new semantics goes a long way toward merging classical and constructive logic. If one sticks to the original Nuprl rules, programs can be still be synthesized from proofs. In addition to giving a conventional set-theoretic interpretation of mathematics formalized in Nuprl, the new semantics immediately justifies new rules, such as the law of the excluded middle, and the existence of an epsilon operator. This is enough to fully interpret the simple type theory of HOL. It should also be enough to fully interpret the more expressive type theory of PVS, although this has not yet been worked out.

In addition to integrating classical and constructive notions of functions, the new semantics also combines the respective treatments of equality. Classically, new equalities are introduced by taking equivalence classes. These are accounted for in the semantics, but by themselves they have no computational sense, so, we also have a data constructor $[\cdot]$ that packages a single representative of an equivalence class. An object [e] can be thought of as being usable in place of any equivalence class containing e as a member. Giving a coherent semantic account of both equivalence classes and objects [e] was the most difficult part of the work.

The extended logic should be sufficient to interpret the logics of most, if not all, existing theorem-proving systems, even the calculus of constructions, via the set-theoretic interpretation given by Werner [35].

However, there is room for substantial improvement, and this will require new theoretical work. The new semantics, as is, rules out ``intersection types''. For example, the intersection, over all types A, of $A \rightarrow A$, is empty in set theory, but in a programming language context we want it to contain the polymorphic identity function $\lambda x. x$. The intersection type is useful for expressing implicit polymorphism and for representing features of object-oriented programming languages.

It would also be useful to have a recursive type constructor along the lines of Mendler [23]. This can be justified in the original semantics, but in the new semantics it is ruled out on grounds of impredicativity. Finally, it may be possible to extend the new semantics, possibly by trying to incorporate more of the old semantics, in order to gain some of the impredicative expressive power of the logics studied by Mason and Talcott (e.g. see [34]).