Max/plus tree automata for termination of term rewriting
We use weighted tree automata as certificates for termination of term rewriting systems. The weights are taken from the arctic semiring: natural numbers extended with ∞ , with the operations "max" and "plus". In order to find and validate these certificates automatically, we rest...
Main Authors: | , |
---|---|
Format: | Article in Journal/Newspaper |
Language: | English |
Published: |
University of Szeged, Institute of Informatics
2009
|
Subjects: | |
Online Access: | https://cyber.bibl.u-szeged.hu/index.php/actcybern/article/view/3772 |
id |
ftjactacyberneti:oai:ojs2.cyber.bibl.u-szeged.hu:article/3772 |
---|---|
record_format |
openpolar |
spelling |
ftjactacyberneti:oai:ojs2.cyber.bibl.u-szeged.hu:article/3772 2023-05-15T14:50:26+02:00 Max/plus tree automata for termination of term rewriting Koprowski, Adam Waldmann, Johannes 2009-01-01 application/pdf https://cyber.bibl.u-szeged.hu/index.php/actcybern/article/view/3772 eng eng University of Szeged, Institute of Informatics https://cyber.bibl.u-szeged.hu/index.php/actcybern/article/view/3772/3756 https://cyber.bibl.u-szeged.hu/index.php/actcybern/article/view/3772 Acta Cybernetica; Vol 19 No 2 (2009); 357-392 2676-993X 0324-721X info:eu-repo/semantics/article info:eu-repo/semantics/publishedVersion 2009 ftjactacyberneti 2022-12-11T16:18:46Z We use weighted tree automata as certificates for termination of term rewriting systems. The weights are taken from the arctic semiring: natural numbers extended with ∞ , with the operations "max" and "plus". In order to find and validate these certificates automatically, we restrict their transition functions to be representable by matrix operations in the semiring. The resulting class of weighted tree automata is called path-separated. This extends the matrix method for term rewriting and the arctic matrix method for string rewriting. In combination with the dependency pair method, this allows for some conceptually simple termination proofs in cases where only much more involved proofs were known before. We further generalize to arctic numbers "below zero": integers extended with ∞. This allows to treat some termination problems with symbols that require a predecessor semantics. Correctness of this approach has been formally verified in the Coq proof assistant and the formalization has been contributed to the CoLoR library of certified termination techniques. This allows formal verification of termination proofs using the arctic matrix method in combination with the dependency pair transformation. This contribution brought a substantial performance gain in the certified category of the 2008 edition of the termination competition. The method has been implemented by leading termination provers. We report on experiments with its implementation in one such tool, Matchbox, developed by the second author. We also show that our method can simulate a previous method of quasiperiodic interpretations, if restricted to interpretations of slope one on unary signatures. Article in Journal/Newspaper Arctic Acta Cybernetica (E-Journal) Arctic |
institution |
Open Polar |
collection |
Acta Cybernetica (E-Journal) |
op_collection_id |
ftjactacyberneti |
language |
English |
description |
We use weighted tree automata as certificates for termination of term rewriting systems. The weights are taken from the arctic semiring: natural numbers extended with ∞ , with the operations "max" and "plus". In order to find and validate these certificates automatically, we restrict their transition functions to be representable by matrix operations in the semiring. The resulting class of weighted tree automata is called path-separated. This extends the matrix method for term rewriting and the arctic matrix method for string rewriting. In combination with the dependency pair method, this allows for some conceptually simple termination proofs in cases where only much more involved proofs were known before. We further generalize to arctic numbers "below zero": integers extended with ∞. This allows to treat some termination problems with symbols that require a predecessor semantics. Correctness of this approach has been formally verified in the Coq proof assistant and the formalization has been contributed to the CoLoR library of certified termination techniques. This allows formal verification of termination proofs using the arctic matrix method in combination with the dependency pair transformation. This contribution brought a substantial performance gain in the certified category of the 2008 edition of the termination competition. The method has been implemented by leading termination provers. We report on experiments with its implementation in one such tool, Matchbox, developed by the second author. We also show that our method can simulate a previous method of quasiperiodic interpretations, if restricted to interpretations of slope one on unary signatures. |
format |
Article in Journal/Newspaper |
author |
Koprowski, Adam Waldmann, Johannes |
spellingShingle |
Koprowski, Adam Waldmann, Johannes Max/plus tree automata for termination of term rewriting |
author_facet |
Koprowski, Adam Waldmann, Johannes |
author_sort |
Koprowski, Adam |
title |
Max/plus tree automata for termination of term rewriting |
title_short |
Max/plus tree automata for termination of term rewriting |
title_full |
Max/plus tree automata for termination of term rewriting |
title_fullStr |
Max/plus tree automata for termination of term rewriting |
title_full_unstemmed |
Max/plus tree automata for termination of term rewriting |
title_sort |
max/plus tree automata for termination of term rewriting |
publisher |
University of Szeged, Institute of Informatics |
publishDate |
2009 |
url |
https://cyber.bibl.u-szeged.hu/index.php/actcybern/article/view/3772 |
geographic |
Arctic |
geographic_facet |
Arctic |
genre |
Arctic |
genre_facet |
Arctic |
op_source |
Acta Cybernetica; Vol 19 No 2 (2009); 357-392 2676-993X 0324-721X |
op_relation |
https://cyber.bibl.u-szeged.hu/index.php/actcybern/article/view/3772/3756 https://cyber.bibl.u-szeged.hu/index.php/actcybern/article/view/3772 |
_version_ |
1766321459410501632 |