Abstract

Matrix interpretations are a powerful technique for proving termination of
term rewrite systems, which is based on the well-known paradigm of
interpreting terms into a domain equipped with a suitable well-founded
order, such that every rewrite step causes a strict decrease.
Traditionally, one uses vectors of non-negative numbers as domain, where
two vectors are in the order relation if there is a strict decrease in the
respective first components and a weak decrease in all other components.
In this paper, we study various alternative well-founded orders on vectors
of non-negative numbers based on vector norms and compare the resulting
variants of matrix interpretations to each other and to the traditional
approach. These comparisons are mainly theoretical in nature. We do,
however, also identify one of these variants as a proper generalization of
traditional matrix interpretations as a stand-alone termination method,
which has the additional advantage that it gives rise to a more powerful
implementation.

BibTeX

@inproceedings{FNAM-RTA11,
  author    = "Friedrich Neurauter and Aart Middeldorp",
  title     = "Revisiting Matrix Interpretations for Proving Termination
               of Term Rewriting",
  booktitle = "Proceedings of the 22nd International Conference on Rewriting
               Techniques and Applications",
  series    = "Leibniz International Proceedings in Informatics",
  volume    = 10,
  pages     = "251--266",
  year      = 2011
}