Cornell University
Library
Cornell UniversityLibrary

eCommons

Help
Log In(current)
  1. Home
  2. Cornell Computing and Information Science
  3. Computer Science
  4. Computer Science Technical Reports
  5. Partial Objects in Constructive Type Theory

Partial Objects in Constructive Type Theory

File(s)
87-822.pdf (1.46 MB)
87-822.ps (352.23 KB)
Permanent Link(s)
https://hdl.handle.net/1813/6662
Collections
Computer Science Technical Reports
Author
Constable, Robert L.
Smith, Scott Fraser
Abstract

Constructive type theories generally treat only total functions; partial functions present serious difficulties. In this paper, a theory of partial objects is given which puts partial functions in a general context. Semantic foundations for the theory are given in terms of a theory of inductive relations. The domain of convergence of a partial function is exactly characterized by a predicate within the theory, allowing for abstract reasoning about termination. Induction principles are given for reasoning about these functions, and comparisons are made to the domain theoretic account of LCF. Finally, an undecidability result is presented to suggest connections to a subset of recursive function theory.

Date Issued
1987-03
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-822
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

copyright © 2002-2026 Cornell University Library | Privacy | Web Accessibility Assistance