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 }