dc.contributor.author Constable, Robert L. en_US dc.date.accessioned 2007-04-23T16:47:31Z dc.date.available 2007-04-23T16:47:31Z dc.date.issued 1983-03 en_US dc.identifier.citation http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR83-549 en_US dc.identifier.uri https://hdl.handle.net/1813/6389 dc.description.abstract Partial functions abound in modern computing theory, and so any system which purports to naturally formalize it must treat them. Surprisingly, the most common treatments do not work well for constructive formal systems, i.e., for those with computational content. Since constructive formal systems are significant in computer science, it is important to give an account of partial functions in them. This paper does that by construing a partial function $\phi :N \rightarrow N$ as a total function $f:D_{f}\rightarrow N$ for $D_{f}$ an inductively defined set generated simultaneously with $f$. This idea has appeared in other guises, at least in the author's previous work, but here it is presented in a pure form. It is compared to Scott's method of using total functions on domains. A formal system of arithmetic is defined to illustrate the ideas. The system is shown consistent relative to constructive type theory; from this result important corollaries are drawn about using the theory as a programming language. KEY WORDS AND PHRASES: automated logic, Heyting arithmetic, constructivity, intuitionistic predicate calculus, partial functions, recursive functions, programming logics, program verification, type theory, type checking. en_US dc.format.extent 1538168 bytes dc.format.extent 371480 bytes dc.format.mimetype application/pdf dc.format.mimetype application/postscript dc.language.iso en_US en_US dc.publisher Cornell University en_US dc.subject computer science en_US dc.subject technical report en_US dc.title Partial Functions in Constructive Formal Theories en_US dc.type technical report en_US
﻿