Abstract
We give two finite axiomatizations of indexed inductive-recursive definitions in intuitionistic type theory. They extend our previous finite axiomatizations of inductive-recursive definitions of sets to indexed families of sets and encompass virtually all definitions of sets which have been used in intuitionistic type theory. The more restricted of the two axiomatization arises naturally by considering indexed inductive-recursive definitions as initial algebras in slice categories, whereas the other admits a more general and convenient form of an introduction rule.
The class of indexed inductive-recursive definitions properly contains the class of indexed inductive definitions (so called “inductive families”). Such definitions are ubiquitous when using intuitionistic type theory for formalizing mathematics and program correctness. A side effect of the present paper is to get compact finite axiomatizations of indexed inductive definitions in intuitionistic type theory as special cases.
Proper indexed inductive-recursive definitions (those which do not correspond to indexed inductive definitions) are useful in intuitionistic metamathematics, and as an example we formalize Tait-style computability predicates for dependent types. We also show that Palmgren’s prooftheoretically strong construction of higher-order universes is an example of a proper indexed inductive-recursive definition. A third interesting example is provided by Bove and Capretta’s definition of termination predicates for functions defined by nested recursion.
Our axiomatizations form a powerful foundation for generic programming with dependent types by introducing a type of codes for indexed inductive-recursive definitions and making it possible to define generic functions by recursion on this type.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
P. Aczel. Frege Structures and the Notions of Proposition, Truth, and Set, pages 31–59. North-Holland, 1980.
T. Altenkirch, V. Gaspes, B. Nordström, and B. von Sydow. A user’s guide to ALF. http://www.www.cs.chalmers.se/ComputingScience/Research/ Logic/alf/guide.html URL, 1996.
A. Bove and V. Capretta. Nested general recursion and partiality in type theory. To appear in the Proceedings of TPHOL 2001.
C. Coquand. Agda. 2000. http://www.cs.chalmers.se/catarina/agda/.
C. Coquand. A realizability interpretation of Martin-Löf’s type theory. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998.
P. Dybjer. Inductive sets and families in Martin-Löf’s type theory and their settheoretic semantics. In G. Huet and G. Plotkin, editors, Logical Frameworks, pages 280–306. Cambridge University Press, 1991.
P. Dybjer. Inductive families. Formal Aspects of Computing, 6:440–465, 1994.
P. Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. Journal of Symbolic Logic, 65(2), June 2000.
P. Dybjer and A. Setzer. A finite axiomatization of inductive-recursive definitions. In J.-Y. Girard, editor, Typed Lambda Calculi and Applications, volume 1581 of Lecture Notes in Computer Science, pages 129–146. Springer, April 1999.
P. Dybjer and A. Setzer. Induction-recursion and initial algebras. Submitted for publication, April 2000.
P. Dybjer and A. Setzer. Indexed induction-recursion. To appear as a Report of Institut Mittag-Leffler, 2001.
L. Magnusson and B. Nordström. The ALF proof editor and its proof engine. In Types for proofs and programs, volume 806 of Lecture Notes in Computer Science, pages 213–317. Springer, 1994.
P. Martin-Löf. An intuitionistic theory of types: Predicative part. In H. E. Rose and J. C. Shepherdson, editors, Logic Colloquium ‘73, pages 73–118. North-Holland, 1975.
P. Martin-Löf. Constructive mathematics and computer programming. In Logic, Methodology and Philosophy of Science, VI, 1979, pages 153–175. North-Holland, 1982.
P. Martin-Löf. On the meaning of the logical constants and the justification of the logical laws, 1983. Notes from a series of lectures given in Siena.
P. Martin-Löf. Intuitionistic Type Theory. Bibliopolis, 1984.
P. Martin-Löf. An intuitionistic theory of types. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998.Reprinted version of an unpublished report from 1972.
B. Nordström, K. Petersson, and J. Smith. Programming in Martin-Löf’s Type Theory: an Introduction. Oxford University Press, 1990.
E. Palmgren. On Fixed Point Operators, Inductive Definitions and Universes in Martin-Löf’ s Type Theory. PhD thesis, Uppsala University, 1991.
E. Palmgren. On universes in type theory. In G. Sambin and J. Smith, editors, Twenty-Five Years of Constructive Type Theory. Oxford University Press, 1998.
C. Paulin-Mohring. Inductive definitions in the system Coq-rules and properties. In Proceedings Typed λ-Calculus and Applications, pages 328-245. Springer-Verlag, LNCS, March 1993.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dybjer, P., Setzer, A. (2001). Indexed Induction-Recursion. In: Kahle, R., Schroeder-Heister, P., Stärk, R. (eds) Proof Theory in Computer Science. PTCS 2001. Lecture Notes in Computer Science, vol 2183. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45504-3_7
Download citation
DOI: https://doi.org/10.1007/3-540-45504-3_7
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42752-0
Online ISBN: 978-3-540-45504-2
eBook Packages: Springer Book Archive