Admissibility of Fixpoint Induction over Partial Types

10 years 1 months ago
Admissibility of Fixpoint Induction over Partial Types
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 xpoint induction. However, xpoint 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 di culties in applying partial types to theorem proving in practice. I also present a general least upper bound theorem for xed points with regard to a computational approximation r...
Karl Crary
Added 05 Aug 2010
Updated 05 Aug 2010
Type Conference
Year 1998
Where CADE
Authors Karl Crary
Comments (0)