For
anyone doing mathematics or programming, recursive definition
needs no motivation;
its expressiveness, elegance and computational
efficiency motivate us to
include forms of it in the Nuprl
logic.
Current work on extending the logic involves three type constructors:
` rec` , the * inductive type constructor*, permitting
inductive data types and predicates;
` inf` , the * lazy type constructor*,
permitting infinite objects;
and `>`

, the * partial
function space constructor*,
permitting recursively defined partial functions.
This chapter gives the extensions to the system necessary for inductive types
and for partial function types;
for detailed presentations of these two types see [Constable & Mendler 85].

- Inductive Types
- Details of the Extension
- Example Proof
- Partial Function Types
- Details of the Extension

Thu Sep 14 08:45:18 EDT 1995