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

A. Geser, D. Hofbauer, J. Waldmann, H. Zantema

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

11 Citations (Scopus)
2 Downloads (Pure)

Abstract

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.
Original languageEnglish
Title of host publicationRewriting Techniques and Applications (Proceedings 16th International Conference, RTA 2005, Nara, Japan, April 19-21, 2005)
EditorsJ. Giesl
Place of PublicationBerlin
PublisherSpringer
Pages353-367
ISBN (Print)3-540-25596-6
DOIs
Publication statusPublished - 2005

Publication series

NameLecture Notes in Computer Science
Volume3467
ISSN (Print)0302-9743

Fingerprint

Dive into the research topics of 'On tree automata that certify termination of left-linear term rewriting systems'. Together they form a unique fingerprint.

Cite this