This approach to partial functions has not been retained in standard Nuprl developments. See Recursive Types for supplementary material and Recursive Functions for more current practice.

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