License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2011.251
URN: urn:nbn:de:0030-drops-31222
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2011/3122/
Go to the corresponding LIPIcs Volume Portal

Neurauter, Friedrich ; Middeldorp, Aart

Revisiting Matrix Interpretations for Proving Termination of Term Rewriting

pdf-format:
15.pdf (0.6 MB)

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 - Entry

@InProceedings{neurauter_et_al:LIPIcs:2011:3122,
  author =	{Friedrich Neurauter and Aart Middeldorp},
  title =	{{Revisiting Matrix Interpretations for Proving Termination of Term Rewriting}},
  booktitle =	{22nd International Conference on Rewriting Techniques and Applications (RTA'11)},
  pages =	{251--266},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-30-9 },
  ISSN =	{1868-8969},
  year =	{2011},
  volume =	{10},
  editor =	{Manfred Schmidt-Schau{\ss}},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2011/3122},
  URN =		{urn:nbn:de:0030-drops-31222},
  doi =		{10.4230/LIPIcs.RTA.2011.251},
  annote =	{Keywords: term rewriting, termination, matrix interpretations}
}

Keywords: term rewriting, termination, matrix interpretations
Collection: 22nd International Conference on Rewriting Techniques and Applications (RTA'11)
Issue Date: 2011
Date of publication: 26.04.2011

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI