Advertisement

Admissibility of fixpoint induction over partial types

  • Karl Crary
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1421)

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 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. [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. [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. [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. [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. [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. [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. [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. [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. [9]
    T. Coquand and G. Huet. The calculus of constructions. Information and Computation, 76:95–120, 1988.MathSciNetCrossRefzbMATHGoogle Scholar
  10. [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. [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. [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. [13]
    R. Harper. Constructing type systems over an operational semantics. Journal of Symbolic Computation, 14:71–84, 1992.zbMATHMathSciNetCrossRefGoogle Scholar
  14. [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. [15]
    D. J. Howe. Equality in lazy computation systems. In Fourth IEEE Symposium on Logic in Computer Science, 1989.Google Scholar
  16. [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. [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. [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. [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. [20]
    L. C. Paulson. Logic and Computation: Interactive Proof with Cambridge LCF. Cambridge University Press, 1987.Google Scholar
  21. [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. [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. [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. [24]
    S. F. Smith. Partial Objects in Type Theory. PhD thesis, Department of Computer Science, Cornell University, Ithaca, New York, Jan. 1989.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1998

Authors and Affiliations

  • Karl Crary
    • 1
  1. 1.Cornell UniversityUSA

Personalised recommendations