Skip to main content
Top
Published in: Journal of Automated Reasoning 4/2022

25-07-2022

Tuple Interpretations for Termination of Term Rewriting

Author: Akihisa Yamada

Published in: Journal of Automated Reasoning | Issue 4/2022

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

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) CrossRefMATH Baader, F., Nipkow, T.: Term Rewriting and All That. Cambridge University Press, Cambridge (1998) CrossRefMATH
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 / Issue 4/2022
Print ISSN: 0168-7433
Electronic ISSN: 1573-0670
DOI
https://doi.org/10.1007/s10817-022-09640-4

Other articles of this Issue 4/2022

Journal of Automated Reasoning 4/2022 Go to the issue

Premium Partner