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 restrict their transiti...
| Main Authors: | , |
|---|---|
| Other Authors: | |
| Format: | Text |
| Language: | English |
| Published: |
2009
|
| Subjects: | |
| Online Access: | http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.429.8381 http://www.inf.u-szeged.hu/actacybernetica/edb/vol19n2/pdf/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 |
|---|