Show simple item record

dc.contributor.authorConstable, Robert L.en_US
dc.description.abstractPartial 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.extent1538168 bytes
dc.format.extent371480 bytes
dc.publisherCornell Universityen_US
dc.subjectcomputer scienceen_US
dc.subjecttechnical reporten_US
dc.titlePartial Functions in Constructive Formal Theoriesen_US
dc.typetechnical reporten_US

Files in this item


This item appears in the following Collection(s)

Show simple item record