Abstract
In a previous work, the first author extended to higher-order rewriting and dependent types the use of size annotations in types, a termination proof technique called type or size based termination and initially developed for ML-like programs. Here, we go one step further by considering conditional rewriting and explicit quantifications and constraints on size annotations. This allows to describe more precisely how the size of the output of a function depends on the size of its inputs. Hence, we can check the termination of more functions. We first give a general type-checking algorithm based on constraint solving. Then, we give a termination criterion with constraints in Presburger arithmetic. To our knowledge, this is the first termination criterion for higher-order conditional rewriting taking into account the conditions in termination.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abel, A.: Termination and productivity checking with continuous types. In: Hofmann, M.O. (ed.) TLCA 2003. LNCS, vol. 2701, pp. 1–15. Springer, Heidelberg (2003)
Abel, A.: Termination checking with types. Theoretical Informatics and Applications 38(4), 277–319 (2004)
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.: Decidability of Type-Checking in the Calculus of Algebraic Constructions with Size Annotations. In: Ong, L. (ed.) CSL 2005. LNCS, vol. 3634, pp. 135–150. Springer, Heidelberg (2005)
Blanqui, F.: Rewriting modulo in Deduction modulo. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706. Springer, Heidelberg (2003)
Blanqui, F.: Termination and confluence of higher-order rewrite systems. In: Bachmair, L. (ed.) RTA 2000. LNCS, vol. 1833. Springer, Heidelberg (2000)
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.: Definitions by rewriting in the Calculus of Constructions. Mathematical Structures in Computer Science 15(1), 37–92 (2005)
Blanqui, F., Kirchner, C., Riba, C.: On the confluence of λ-calculus with conditional rewriting. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006. LNCS, vol. 3921, pp. 382–397. Springer, Heidelberg (2006)
Chin, W.N., Khoo, S.C.: Calculating sized types. Journal of Higher-Order and Symbolic Computation 14(2-3), 261–300 (2001)
Davies, R., Pfenning, F.: Intersection types and computational effects. In: Proc. of ICFP 2000, SIGPLAN Notices 35(9) (2000)
Fischer, M., Rabin, M.: Super-exponential complexity of presburger arithmetic. In: Proceedings of the SIAM-AMS Symposium in Applied Mathematics (1974)
Gallier, J.: On Girard’s “Candidats de Réductibilité”. In: Odifreddi, P.-G. (ed.) Logic and Computer Science. North-Holland, Amsterdam (1990)
Hughes, J., Pareto, L., Sabry, A.: Proving the correctness of reactive systems using sized types. In: Proc. of POPL 1996 (1996)
Klop, J.W., van Oostrom, V., van Raamsdonk, F.: Combinatory reduction systems. Theoretical Computer Science 121, 279–308 (1993)
Mayr, R., Nipkow, T.: Higher-order rewrite systems and their confluence. Theoretical Computer Science 192(2), 3–29 (1998)
Presburger, M.: ber die vollst ndigkeit eines gewissen systems der arithmetik ganzer zahlen, in welchem die addition als einzige operation hervortritt. In: Sprawozdanie z I Kongresu Matematykow Krajow Slowcanskich, Warszawa, Poland (1929)
Tait, W.W.: A realizability interpretation of the theory of species. In: Parikh, R. (ed.) AUSCRYPT 1990. Lecture Notes in Mathematics, vol. 453 (1975)
van Oostrom, V., van Raamsdonk, F.: Comparing Combinatory Reduction Systems and Higher-order Rewrite Systems. In: Heering, J., Meinke, K., Möller, B., Nipkow, T. (eds.) HOA 1993. LNCS, vol. 816, Springer, Heidelberg (1994)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
(INRIA), F.B., (INPL), C.R. (2006). Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems. In: Hermann, M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2006. Lecture Notes in Computer Science(), vol 4246. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11916277_8
Download citation
DOI: https://doi.org/10.1007/11916277_8
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-48281-9
Online ISBN: 978-3-540-48282-6
eBook Packages: Computer ScienceComputer Science (R0)