On Tree Automata that Certify Termination of Left-Linear Term Rewriting Systems

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...

• Type: Conference
• Year: 2005
• Where: RTA
• Authors: Alfons Geser, Dieter Hofbauer, Johannes Waldmann, Hans Zantema
• Keywords: Match Bound Method, RTA 2005, Term Rewriting System, Theoretical Computer Science, finite Signature