TY - GEN

T1 - On tree automata that certify termination of left-linear term rewriting systems

AU - Geser, A.

AU - Hofbauer, D.

AU - Waldmann, J.

AU - Zantema, H.

PY - 2005

Y1 - 2005

N2 - We present a new method for proving termination of term rewriting systems automatically. It is a generalization of the match bound method for string rewriting. To prove that a term rewriting system terminates on a given regular language of terms, we first construct an enriched system over a new signature that simulates the original derivations. The enriched system is an infinite system over an infinite signature, but it is locally terminating: every restriction of the enriched system to a finite signature is terminating. We then construct iteratively a finite tree automaton that accepts the enriched given regular language and is closed under rewriting modulo the enriched system. If this procedure stops, then the enriched system is compact: every enriched derivation involves only a finite signature. Therefore, the original system terminates. We present three methods to construct the enrichment: top heights, roof heights, and match heights. Top and roof heights work for left-linear systems, while match heights give a powerful method for linear systems. For linear systems, the method is strengthened further by a forward closure construction. Using these methods, we give examples for automated termination proofs that cannot be obtained by standard methods.

AB - We present a new method for proving termination of term rewriting systems automatically. It is a generalization of the match bound method for string rewriting. To prove that a term rewriting system terminates on a given regular language of terms, we first construct an enriched system over a new signature that simulates the original derivations. The enriched system is an infinite system over an infinite signature, but it is locally terminating: every restriction of the enriched system to a finite signature is terminating. We then construct iteratively a finite tree automaton that accepts the enriched given regular language and is closed under rewriting modulo the enriched system. If this procedure stops, then the enriched system is compact: every enriched derivation involves only a finite signature. Therefore, the original system terminates. We present three methods to construct the enrichment: top heights, roof heights, and match heights. Top and roof heights work for left-linear systems, while match heights give a powerful method for linear systems. For linear systems, the method is strengthened further by a forward closure construction. Using these methods, we give examples for automated termination proofs that cannot be obtained by standard methods.

U2 - 10.1007/978-3-540-32033-3_26

DO - 10.1007/978-3-540-32033-3_26

M3 - Conference contribution

SN - 3-540-25596-6

T3 - Lecture Notes in Computer Science

SP - 353

EP - 367

BT - Rewriting Techniques and Applications (Proceedings 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005)

A2 - Giesl, J.

PB - Springer

CY - Berlin

ER -