Max/plus tree automata for termination of term rewriting

• Main Authors: Adam Koprowski, Johannes Waldmann
• Other Authors: The Pennsylvania State University CiteSeerX Archives
• Format: Text
• Language: English
• Published: 2009
• Subjects: term rewriting; termination; weighted tree automaton; max/plus algebra; arctic semiring; monotone algebra; matrix interpretation; formal verification; Arctic
• 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

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