next up previous contents index
Next: Inductive Types Up: No Title Previous: Denotational Semantics

Recursive Definition

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].

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