On Forward Closure and the Finite Variant Property

摘要

Equational unification is an important research area with many applications, such as cryptographic protocol analysis. Unification modulo a convergent term rewrite system is undecidable, even with just a single rule. To identify decidable (and tractable) cases, two paradigms have been developed - Basic Syntactic Mutation [14] and the Finite Variant Property [6]. Inspired by the Basic Syntactic Mutation approach, we investigate the notion of forward closure along with suitable redundancy constraints. We show that a convergent term rewriting system R has a finite forward closure if and only if R has the finite variant property. We also show the undecidability of the finiteness of forward closure, therefore determining if a system has the finite variant property is undecidable.