### On the Domain and Dimension Hierarchy of Matrix Interpretations

Friedrich Neurauter and Aart MiddeldorpProceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR-18), Lecture Notes in Artificial Intelligence (Advanced Research in Computing and Software Science) 7180, pp. 320 – 334, 2012.

### Abstract

Matrix interpretations are a powerful technique for proving termination of

term rewrite systems. Depending on the underlying domain of interpretation,

one distinguishes between matrix interpretations over the real, rational

and natural numbers. In this paper we clarify the relationship between all

three variants, showing that matrix interpretations over the reals are more

powerful than matrix interpretations over the rationals, which are in turn

more powerful than matrix interpretations over the natural numbers. We also

clarify the ramifications of matrix dimension on termination proving power.

To this end, we establish a hierarchy of matrix interpretations with

respect to matrix dimension and show it to be infinite, with each level

properly subsuming its predecessor.

### BibTeX

@inproceedings{FNAM-LPAR18, author = "Friedrich Neurauter and Aart Middeldorp", title = "On the Domain and Dimension Hierarchy of Matrix Interpretations", booktitle = "Proceedings of the 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning", series = "Lecture Notes in Computer Science (Advanced Research in Computing and Software Science)", volume = 7180, pages = "320--334", year = 2012 }