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 Entry

@inproceedings{NM-LPAR12,
 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,
 doi       = "10.1007/978-3-642-28717-6\_25"
}