DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2026.32

New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations

Authors: René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, and Johannes Waldmann

Published in: LIPIcs, Volume 378, 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)

Abstract

We provide new proofs of two important theorems for proving termination of term rewrite systems (TRSs), including a full formalization in Isabelle/HOL. We first consider Dershowitz' theorem that termination starting from arbitrary terms is equivalent to termination starting from terms in the right-forward closures of right-hand sides, provided that the TRS is right-linear or orthogonal. Our new proof deviates from the original one in that no reorderings of steps in infinite derivations are required, making it more precise in its argumentation. It also subsumes a later result that one can weaken orthogonality to locally confluent overlay TRSs. The second theorem is about matrix interpretations. These were introduced by Hofbauer and Waldmann for proving termination of string rewrite systems (SRSs), internally using the concept of a core. Subsequently, Endrullis, Waldmann and Zantema developed matrix interpretations for TRSs without using the idea of a core. Whereas matrix interpretations for TRSs have already been formalized several times, so far this was not the case for core SRS matrix interpretations. We not only provide such a formalization, but also extend core SRS matrix interpretations to TRSs. These new core matrix interpretations for TRSs generalize previous approaches.

Cite as

René Thiemann, Dieter Hofbauer, Ulysse Le Huitouze, and Johannes Waldmann. New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 32:1-32:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{thiemann_et_al:LIPIcs.FSCD.2026.32,
  author =	{Thiemann, Ren\'{e} and Hofbauer, Dieter and Le Huitouze, Ulysse and Waldmann, Johannes},
  title =	{{New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations}},
  booktitle =	{11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026)},
  pages =	{32:1--32:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-433-8},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{378},
  editor =	{Pfenning, Frank},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2026.32},
  URN =		{urn:nbn:de:0030-drops-263825},
  doi =		{10.4230/LIPIcs.FSCD.2026.32},
  annote =	{Keywords: Isabelle/HOL, Matrix Interpretations, Narrowing, Right-Forward Closures, Term Rewriting}
}

Search Results

Documents authored by Le Huitouze, Ulysse

New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations

Abstract

Cite as

Thanks for your feedback!

Could not send message