|
eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >
Please use this identifier to cite or link to this item:
http://hdl.handle.net/1813/6662
| Title: | Partial Objects in Constructive Type Theory |
| Authors: | Constable, Robert L.
Smith, Scott Fraser |
| Keywords: | computer science
technical report |
| Issue Date: | Mar-1987 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR87-822 |
| 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. |
| URI: | http://hdl.handle.net/1813/6662 |
| Appears in Collections: | Computer Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
