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. Admissibility of Fixpoint Induction over Partial Types

Admissibility of Fixpoint Induction over Partial Types

File(s)
98-1674.pdf (233.3 KB)
98-1674.ps (457.11 KB)
Permanent Link(s)
https://hdl.handle.net/1813/7328
Collections
Computer Science Technical Reports
Author
Crary, Karl
Abstract

Partial types allow the reasoning about partial functions in type theory. The partial functions of main interest are recursively computed functions, which are commonly assigned types using fixpoint induction. However, fixpoint induction is valid only on admissible types. Previous work has shown many types to be admissible, but has not shown any dependent products to be admissible. Disallowing recursion on dependent product types substantially reduces the expressiveness of the logic; for example, it prevents much reasoning about modules, objects and algebras. In this paper I present two new tools, predicate-admissibility and monotonicity, for showing types to be admissible. These tools show a wide class of types to be admissible; in particular, they show many dependent products to be admissible. This alleviates difficulties in applying partial types to theorem proving in practice. I also present a general least upper bound theorem for fixed points with regard to a computational approximation relation, and show an elegant application of the theorem to compactness.

Date Issued
1998-04
Publisher
Cornell University
Keywords
computer science
•
technical report
Previously Published as
http://techreports.library.cornell.edu:8081/Dienst/UI/1.0/Display/cul.cs/TR98-1674
Type
technical report

Site Statistics | Help

About eCommons | Policies | Terms of use | Contact Us

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