cl-banner

On the Domain and Dimension Hierarchy of Matrix Interpretations

Friedrich Neurauter and Aart Middeldorp

Proceedings 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.

 

  PDF |    doi:10.1007/978-3-642-28717-6_25  |  ©  Springer

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
}
Nach oben scrollen