Max/plus tree automata for termination of term rewriting

Koprowski, Adam and Waldmann, Johannes: Max/plus tree automata for termination of term rewriting. Acta cybernetica, (19) 2. pp. 357-392. (2009)

[img] Cikk, tanulmány, mű
Koprowski_2009_ActaCybernetica.pdf

Download (260kB)

Abstract

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.

Item Type: Article
Event Title: Weighted Automata: Theory and Applications, 2008, Dresden
Journal or Publication Title: Acta cybernetica
Date: 2009
Volume: 19
Number: 2
Page Range: pp. 357-392
ISSN: 0324-721X
Language: angol
Uncontrolled Keywords: Természettudomány, Informatika
Additional Information: Bibliogr.: p. 389-392.; Abstract
Date Deposited: 2016. Oct. 15. 12:25
Last Modified: 2018. Jun. 06. 10:17
URI: http://acta.bibl.u-szeged.hu/id/eprint/12869

Actions (login required)

View Item View Item