Termination Modulo Combinations of Equational Theories

Duran, Francisco; Lucas, Salvador; Meseguer, José

Permalink

https://hdl.handle.net/2142/12311 Copy

Description

Title

Termination Modulo Combinations of Equational Theories

Author(s)

• Duran, Francisco
• Lucas, Salvador
• Meseguer, José

Issue Date

2009-06-19

Keyword(s)

term rewriting, termination, modularity

Abstract

Rewriting with rules R modulo axioms E is a widely used technique in both rule-based programming languages and in automated deduction. Termination methods for rewriting systems modulo specific axioms E (e.g., associativity-commutativity) are known. However, much less seems to be known about termination methods that can be modular in the set E of axioms. In fact, current termination tools and proof methods cannot be applied to commonly occurring combinations of axioms that fall outside their scope. This work proposes a modular termination proof method based on semantics- and termination-preserving transformations that can reduce the proof of termination of rules R modulo E to an equivalent proof of termination of the transformed rules modulo a typically much simpler set B of axioms. Our method is based on the notion of variants of a term recently proposed by Comon and Delaune. We illustrate its practical usefulness by considering the very common case in which E is an arbitrary combination of associativity, commutativity, left- and right-identity axioms for various function symbols.

Type of Resource

text

Language

en

Permalink

http://hdl.handle.net/2142/12311

Sponsor(s)/Grant Number(s)

F. Dur ́an and S. Lucas were partially supported by Spanish MEC under grants TIN 2008-03107 and TIN 2007-68093-C02, respectively. J. Meseguer was partially supported by NSF Grants CNS 07-16638 and CNS 08-31064.

Owning Collections