     Next: Introduction Rules Up: Appendix B: Converting Previous: Appendix B: Converting

# Differences in the Logic

The Nuprl proof rules naturally extend the Lambda--prl proof rules and as such are organized along roughly the same lines. However, the logic of Nuprl is considerably more powerful than that of Lambda--prl , and the rules are correspondingly more complex. The Nuprl rules are classified into three broad categories: introduction, elimination and equality; the equality rules are further broken down into computation rules and equality rules for each of the term constructors. The introduction and elimination rules are analogous to those in Lambda--prl ; the equality rules are a new feature of the Nuprl logic.

The differences between the logic of Lambda--prl and Nuprl can be briefly summarized as follows:

• Strengthening the type structure.
The Lambda--prl logic is based on two primitive types, integers and lists of integers. The Nuprl logic extends this to a much richer type structure.
• Identifying propositions with types.
In Lambda--prl propositions were specific syntactic entities. In Nuprl propositions are simply certain kinds of types. Demonstrating the truth of a proposition amounts to presenting an object of that type so that a proposition is treated as the type of its justifications.
• Well-formedness.
In Lambda--prl well--formedness of propositions was checked by the system. The richness of the Nuprl type structure, however, precludes the possibility of automatically checking whether or not an expression is a type. By the identification of propositions with types this property extends to propositions as well.
• Explicit treatment of equality and simplification.
In Lambda--prl equality and simplification were by and large taken care of by the arith rule, which handled simple arithmetic, substitutivity of equality and simplification of terms (such as hd[1,2]=1). The Nuprl logic, however, is sufficiently rich that such a treatment is no longer possible. Consequently there are rules for equality of terms and for computation.
We now discuss the effect of these aspects of the Nuprl logic on the formulation of the rules.     Next: Introduction Rules Up: Appendix B: Converting Previous: Appendix B: Converting

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995