Abstract
Since Val Tannen’s pioneering work on the combination of simply-typed λ-calculus and first-order rewriting [11], many authors have contributed to this subject by extending it to richer typed λ-calculi and rewriting paradigms, culminating in the Calculus of Algebraic Constructions. These works provide theoretical foundations for type-theoretic proof assistants where functions and predicates are defined by oriented higher-order equations. This kind of definitions subsumes usual inductive definitions, is easier to write and provides more automation.
On the other hand, checking that such user-defined rewrite rules, when combined with β-reduction, are strongly normalizing and confluent, and preserve the decidability of type-checking, is more difficult. Most termination criteria rely on the term structure. In a previous work, we extended to dependent types and higher-order rewriting, the notion of “sized types” studied by several authors in the simpler framework of ML-like languages, and proved that it preserves strong normalization.
The main contribution of the present paper is twofold. First, we prove that, in the Calculus of Algebraic Constructions with size annotations, the problems of type inference and type-checking are decidable, provided that the sets of constraints generated by size annotations are satisfiable and admit most general solutions. Second, we prove the latter properties for a size algebra rich enough for capturing usual induction-based definitions and much more.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Abel, A.: Termination checking with types. Theoretical Informatics and Applications 38(4), 277–319 (2004)
Barendregt, H.: Lambda calculi with types. In: Abramsky, S., Gabbay, D., Maibaum, T. (eds.) Handbook of logic in computer science, vol. 2, Oxford University Press, Oxford (1992)
Barthe, G., Frade, M.J., Giménez, E., Pinto, L., Uustalu, T.: Type-based termination of recursive definitions. Mathematical Structures in Computer Science 14(1), 97–141 (2004)
Barthe, G., Grégoire, B., Pastawski, F.: Practical inference for type-based termination in a polymorphic setting. In: Urzyczyn, P. (ed.) TLCA 2005. LNCS, vol. 3461, pp. 71–85. Springer, Heidelberg (2005)
Blanqui, F.: Rewriting modulo in Deduction modulo. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, Springer, Heidelberg (2003)
Blanqui, F.: A type-based termination criterion for dependently-typed higher-order rewrite systems. In: van Oostrom, V. (ed.) RTA 2004. LNCS, vol. 3091, pp. 24–39. Springer, Heidelberg (2004)
Blanqui,F.: Full version of [6], See http://www.loria.fr/~blanqui/
Blanqui, F.: Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science 15(1), 37–92 (2005)
Blanqui, F.: Full version, See http://www.loria.fr/~blanqui/
Blanqui, F.: Inductive types in the Calculus of Algebraic Constructions. Fundamenta Informaticae 65(1-2), 61–86 (2005)
Breazu-Tannen, V.: Combining algebra and higher-order types. In: Proc. of LICS 1988 (1998)
Chen, G.: Subtyping, Type Conversion and Transitivity Elimination. PhD thesis, Université Paris VII, France (1998)
Chin, W.N., Khoo, S.C.: Calculating sized types. Journal of Higher-Order and Symbolic Computation 14(2-3), 261–300 (2001)
Coq-Development-Team. The Coq Proof Assistant Reference Manual - Version 8.0. INRIA Rocquencourt, France (2004) http://coq.inria.fr/
Coquand, T.: An algorithm for testing conversion in type theory. In: Huet, G., Plotkin, G. (eds.) Logical Frameworks, pp. 255–279. Cambridge University Press, Cambridge (1991)
Coquand, T., Huet, G.: The Calculus of Constructions. Information and Computation 76(2-3), 95–120 (1988)
Coquand, T., Paulin-Mohring, C.: Inductively defined types. In: Martin-Löf, P., Mints, G. (eds.) COLOG 1988. LNCS, vol. 417, Springer, Heidelberg (1990)
Dershowitz, N., Jouannaud, J.-P.: Rewrite systems. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, vol. B, ch. 6, North-Holland, Amsterdam (1990)
Giménez, E.: Structural recursive definitions in type theory. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, p. 397. Springer, Heidelberg (1998)
Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: Proc. of POPL 1996 (1996)
Jouannaud, J.-P., Rubio, A.: The Higher-Order Recursive Path Ordering. In: Proc. of LICS 1999 (1999)
Lueker, G., Megiddo, N., Ramachandran, V.: Linear programming with two variables per inequality in poly-log time. SIAM Journal on Computing 19(6), 1000–1010 (1990)
Müller, F.: Confluence of the lambda calculus with left-linear algebraic rewriting. Information Processing Letters 41(6), 293–299 (1992)
Odersky, M., Sulzmann, M., Wehr, M.: Type inference with constrained types. Theory and Practice of Object Systems 5(1), 35–55 (1999)
Pratt, V.: Two easy theories whose combination is hard. Technical report, MIT, United States (1977)
Sulzmann, M.: A general type inference framework for Hindley/Milner style systems. In: Kuchen, H., Ueda, K. (eds.) FLOPS 2001. LNCS, vol. 2024, p. 248. Springer, Heidelberg (2001)
Walukiewicz-Chrząszcz, D.: Termination of rewriting in the Calculus of Constructions. Journal of Functional Programming 13(2), 339–414 (2003)
Xi, H.: Dependent types in practical programming. PhD thesis, Carnegie-Mellon, Pittsburgh, United States (1998)
Xi, H.: Dependent types for program termination verification. Journal of Higher- Order and Symbolic Computation 15(1), 91–131 (2002)
Zenger, C.: Indexed types. Theoretical Computer Science 187(1-2), 147–165 (1997)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blanqui, F. (2005). Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations. In: Ong, L. (eds) Computer Science Logic. CSL 2005. Lecture Notes in Computer Science, vol 3634. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11538363_11
Download citation
DOI: https://doi.org/10.1007/11538363_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-28231-0
Online ISBN: 978-3-540-31897-2
eBook Packages: Computer ScienceComputer Science (R0)