|
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/6583
| Title: | Infinite Objects in Type Theory |
| Authors: | Mendler, N. P.
Panangaden, Prakash
Constable, Robert L. |
| Keywords: | computer science
technical report |
| Issue Date: | Mar-1986 |
| Publisher: | Cornell University |
| Citation: | http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR86-743 |
| Abstract: | In this paper we show how infinite objects can be defined in a constructive type theory. The type theory that we use is a variant of Martin-Lof's Intuitionistic Type Theory. We show how one can express the intuition that infinite objects are understood through a limiting process without having to introduce partial objects in the theory. This means that we can adhere to the propositions-as-types principle. The type of infinite objects thus contains only total elements. The approximation is expressed through a sequence of types that approximate the type of infinite objects. We give two semantic accounts of types of infinite objects. The first is lattice theoretic and shows how these types can be understood as fixed points. The second is category theoretic and shows the duality between types of infinite objects and the ordinary recursive type definitions. |
| URI: | http://hdl.handle.net/1813/6583 |
| Appears in Collections: | Computer Science Technical Reports
|
Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.
|
