Title:	Recursive Definitions in Type Theory
Authors:	Constable, Robert L. Mendler, N. P.
Keywords:	computer science technical report
Issue Date:	Jan-1985
Publisher:	Cornell University
Citation:	http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR85-659
Abstract:	The type theories we consider are adequate for the foundations of mathematics and computer science. Recursive type definitions are important practical ways to organize data, and they express powerful axioms about the termination of procedures. In the theory examined here, the demands of practicality arising from our implemented system, Nuprl, suggest an approach to recursive types that significantly increases the proof theoretic power of the theory and leads to insights into computational semantics. We offer a new account of recursive definitions for both types and partial functions. The computational requirements of the theory restrict recursive type definitions involving the total function-space constructor ($\rightarrow$) to those with only positive occurrences of the defined type. But we show that arbitrary recursive definitions with respect to the partial function-space constructor are sensible. The partial function-space constructor allows us to express reflexive types of Scott's domain theory (as needed to model the lambda calculus) and thereby reconcile parts of domain theory with constructive type theory.
URI:	http://hdl.handle.net/1813/6499
Appears in Collections:	Computer Science Technical Reports

Files in This Item: File Description Size Format 85-659.pdf 2.22 MB Adobe PDF View/Open 85-659.ps 561.88 kB Postscript View/Open

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.