Search Results

Documents authored by Neurauter, Friedrich

Document
DOI: 10.4230/LIPIcs.RTA.2011.251
Revisiting Matrix Interpretations for Proving Termination of Term Rewriting

Authors: Friedrich Neurauter and Aart Middeldorp

Published in: LIPIcs, Volume 10, 22nd International Conference on Rewriting Techniques and Applications (RTA'11) (2011)

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.
Cite as

Friedrich Neurauter and Aart Middeldorp. Revisiting Matrix Interpretations for Proving Termination of Term Rewriting. In 22nd International Conference on Rewriting Techniques and Applications (RTA'11). Leibniz International Proceedings in Informatics (LIPIcs), Volume 10, pp. 251-266, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@InProceedings{neurauter_et_al:LIPIcs.RTA.2011.251,
  author =	{Neurauter, Friedrich and Middeldorp, Aart},
  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 =	{Schmidt-Schauss, Manfred},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2011.251},
  URN =		{urn:nbn:de:0030-drops-31222},
  doi =		{10.4230/LIPIcs.RTA.2011.251},
  annote =	{Keywords: term rewriting, termination, matrix interpretations}
}
Document
DOI: 10.4230/LIPIcs.RTA.2010.243
Polynomial Interpretations over the Reals do not Subsume Polynomial Interpretations over the Integers

Authors: Friedrich Neurauter and Aart Middeldorp

Published in: LIPIcs, Volume 6, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (2010)

Abstract
Polynomial interpretations are a useful technique for proving termination of term rewrite systems. They come in various flavors: polynomial interpretations with real, rational and integer coefficients. In 2006, Lucas proved that there are rewrite systems that can be shown polynomially terminating by polynomial interpretations with real (algebraic) coefficients, but cannot be shown polynomially terminating using polynomials with rational coefficients only. He also proved a similar theorem with respect to the use of rational coefficients versus integer coefficients. In this paper we show that polynomial interpretations with real or rational coefficients do not subsume polynomial interpretations with integer coefficients, contrary to what is commonly believed. We further show that polynomial interpretations with real coefficients subsume polynomial interpretations with rational coefficients.
Cite as

Friedrich Neurauter and Aart Middeldorp. Polynomial Interpretations over the Reals do not Subsume Polynomial Interpretations over the Integers. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 243-258, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{neurauter_et_al:LIPIcs.RTA.2010.243,
  author =	{Neurauter, Friedrich and Middeldorp, Aart},
  title =	{{Polynomial Interpretations over the Reals do not Subsume Polynomial Interpretations over the Integers}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{243--258},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Lynch, Christopher},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.RTA.2010.243},
  URN =		{urn:nbn:de:0030-drops-26565},
  doi =		{10.4230/LIPIcs.RTA.2010.243},
  annote =	{Keywords: Term rewriting, termination, polynomial interpretations}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact