Skip to main content
main-content
Top

Hint

Swipe to navigate through the articles of this issue

25-07-2022

Tuple Interpretations for Termination of Term Rewriting

Author: Akihisa Yamada

Published in: Journal of Automated Reasoning

Login to get access
share
SHARE

Abstract

Interpretation methods constitute a foundation of the termination analysis of term rewriting. From time to time, remarkable instances of interpretation methods appeared, such as polynomial interpretations, matrix interpretations, arctic interpretations, and their variants. In this paper, we introduce a general framework, the tuple interpretation method, that subsumes these variants as well as many previously unknown interpretation methods as instances. Employing the notion of derivers, we prove the soundness of the proposed method in an elegant way. We implement the proposed method in the termination prover NaTT and verify its significance through experiments.
Footnotes
1
For clarity, we omit the rules that define \(\mathtt{mul}\); the analyses we make on \({\mathcal {R}}_\mathtt{fact}\) later on can be easily extended for coping with those rules.
 
2
In the literature, sorted signatures are given more assumptions such as monotonicity or regularity. For the purpose of this paper, these assumptions are not necessary.
 
Literature
2.
go back to reference Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) CrossRef Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) CrossRef
23.
go back to reference Koprowski, A., Waldmann, J.: Max/plus tree automata for termination of term rewriting. Acta Cybern. 19(2), 357–392 (2009) MathSciNetMATH Koprowski, A., Waldmann, J.: Max/plus tree automata for termination of term rewriting. Acta Cybern. 19(2), 357–392 (2009) MathSciNetMATH
26.
go back to reference Lankford, D.: Canonical algebraic simplification in computational logic. Tech. Rep. ATP-25, University of Texas (1975) Lankford, D.: Canonical algebraic simplification in computational logic. Tech. Rep. ATP-25, University of Texas (1975)
28.
go back to reference Manna, Z., Ness, S.: On the termination of Markov algorithms. In: The 3rd Hawaii International Conference on System Science, pp. 789–792 (1970) Manna, Z., Ness, S.: On the termination of Markov algorithms. In: The 3rd Hawaii International Conference on System Science, pp. 789–792 (1970)
35.
go back to reference Watson, T., Goguen, J., Thatcher, J., Wagner, E.: An initial algebra approach to the specification, correctness, and implementation of abstract data types. In: Current Trends in Programming Methodology. Prentice Hall, Englewood Cliffs (1976) Watson, T., Goguen, J., Thatcher, J., Wagner, E.: An initial algebra approach to the specification, correctness, and implementation of abstract data types. In: Current Trends in Programming Methodology. Prentice Hall, Englewood Cliffs (1976)
Metadata
Title
Tuple Interpretations for Termination of Term Rewriting
Author
Akihisa Yamada
Publication date
25-07-2022
Publisher
Springer Netherlands
Published in
Journal of Automated Reasoning
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-022-09640-4

Premium Partner