Sciweavers

Share
RTA
2005
Springer

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

4 years 5 months ago
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...
Alfons Geser, Dieter Hofbauer, Johannes Waldmann,
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where RTA
Authors Alfons Geser, Dieter Hofbauer, Johannes Waldmann, Hans Zantema
Comments (0)
books