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: | Text |
| Language: | Hungarian English |
| Published: |
2009
|
| Subjects: | |
| Online Access: | http://acta.bibl.u-szeged.hu/12869/ http://acta.bibl.u-szeged.hu/12869/1/Koprowski_2009_ActaCybernetica.pdf |
| Summary: | 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. |
|---|