# Admissibility of fixpoint induction over partial types

## 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.

## Keywords

Canonical Form Type Theory Partial Function Computation System IEEE Symposium## Preview

Unable to display preview. Download preview PDF.

## References

- [1]S. Allen. A non-type-theoretic definition of Martin-Löf's types. In
*Second IEEE Symposium on Logic in Computer Science*, pages 215–221, Ithaca, New York, June 1987.Google Scholar - [2]P. Audebaud. Partial objects in the calculus of constructions. In
*Sixth IEEE Symposium on Logic in Computer Science*, pages 86–95, Amsterdam, July 1991.Google Scholar - [3]B. Barras, S. Boutin, C. Cornes, J. Courant, J.-C. Filliâtre, E. Giménez, H. Herbelin, G. Huet, C. Muñoz, C. Murthy, C. Parent, C. Paulin-Mohring, A. SaÏbi, and B. Werner.
*The Coq Proof Assistant Reference Manual*. INRIA-Rocquencourt, CNRS and ENS Lyon, 1996.Google Scholar - [4]D. A. Basin. An environment for automated reasoning about partial functions. In
*Ninth International Conference on Automated Deduction*, volume 310 of*Lecture Notes in Computer Science*. Springer-Verlag, 1988.Google Scholar - [5]R. Constable, S. Allen, H. Bromley, W. Cleaveland, J. Cremer, R. Harper, D. Howe, T. Knoblock, N. Mendler, P. Panangaden, J. Sasaki, and S. Smith.
*Implementing Mathematics with the Nuprl Proof Development System*. Prentice-Hall, 1986.Google Scholar - [6]R. L. Constable and K. Crary. Computational complexity and induction for partial computable functions in type theory. Technical report, Department of Computer Science, Cornell University, 1997.Google Scholar
- [7]R. L. Constable and S. F. Smith. Partial objects in constructive type theory. In
*Second IEEE Symposium on Logic in Computer Science*, pages 183–193, Ithaca, New York, June 1987.Google Scholar - [8]R. L. Constable and S. F. Smith. Computational foundations of basic recursive function theory. In
*Third IEEE Symposium on Logic in Computer Science*, pages 360–371, Edinburgh, Scotland, July 1988.Google Scholar - [9]T. Coquand and G. Huet. The calculus of constructions.
*Information and Computation*, 76:95–120, 1988.MathSciNetCrossRefzbMATHGoogle Scholar - [10]K. Crary. Admissibility of fixpoint induction over partial types. Technical Report TR98-1674, Department of Computer Science, Cornell University, Apr. 1998.Google Scholar
- [11]K. Crary.
*Type-Theoretic Methodology for Practical Programming Languages*. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, 1998. Forthcoming.Google Scholar - [12]M. J. Gordon, A. J. Milner, and C. P. Wadsworth.
*Edinburgh LCF: A Mechanised Logic of Computation*, volume 78 of*Lecture Notes in Computer Science*. Springer-Verlag, 1979.Google Scholar - [13]R. Harper. Constructing type systems over an operational semantics.
*Journal of Symbolic Computation*, 14:71–84, 1992.zbMATHMathSciNetCrossRefGoogle Scholar - [14]W. Howard. The formulas-as-types notion of construction. In J. P. Seldin and J. R. Hindley, editors,
*To H.B. Curry: Essays on Combinatory Logic, Lambda-Calculus and Formalism*, pages 479–490. Academic Press, 1980.Google Scholar - [15]D. J. Howe. Equality in lazy computation systems. In
*Fourth IEEE Symposium on Logic in Computer Science*, 1989.Google Scholar - [16]S. Igarashi. Admissibility of fixed-point induction in first-order logic of typed theories. Technical Report AIM-168, Computer Science Department, Stanford University, May 1972.Google Scholar
- [17]P. B. Jackson.
*Enhancing the Nuprl Proof Development System and Applying it to Computational Abstract Algebra*. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, Jan. 1995.Google Scholar - [18]D. MacQueen. Using dependent types to express modular structure. In
*Thirteenth ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages*, pages 277–286, St. Petersburg Beach, Florida, Jan. 1986.Google Scholar - [19]P. Martin-Löf. Constructive mathematics and computer programming. In
*Sixth International Congress of Logic, Methodology and Philosophy of Science*, volume 104 of*Studies in Logic and the Foundations of Mathematics*, pages 153–175. North-Holland, 1982.Google Scholar - [20]L. C. Paulson.
*Logic and Computation: Interactive Proof with Cambridge LCF*. Cambridge University Press, 1987.Google Scholar - [21]B. C. Pierce and D. N. Turner. Simple type-theoretic foundations for object-oriented programming.
*Journal of Functional Programming*, 4(2):207–247, Apr. 1994.CrossRefzbMATHGoogle Scholar - [22]D. Scott. Outline of a mathematical theory of computation. In
*Fourth Princeton Conference on Information Sciences and Systems*, pages 169–176, 1970.Google Scholar - [23]D. Scott. Lattice theoretic models for various type-free calculi. In
*Fourth International Congress of Logic, Methodology and Philosophy of Science*. North-Holland, 1972.Google Scholar - [24]S. F. Smith.
*Partial Objects in Type Theory*. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, Jan. 1989.Google Scholar