Unification in a Combination of Arbitrary Disjoint Equational Theories

Abstract

The unification problem of terms in a disjoint combination E1 + ... + En of arbitrary theories is reduced to a combination of pure unification problems in Ej, where free constants may occur in terms, and to constant elimination problems like: find all substitutions σ such that ci is not a constant in the term σti, i = 1,...,n, where ti are terms in the theory Ej. The algorithm consists of the following basic steps: First of all the terms to be unified are transformed via variable abstraction into terms belonging to one particular theory. Terms belonging to the same theory can now be unified with the algorithm for this theory. For terms in some multi-equation belonging to different theories it is sufficient to select some theory and collapse all terms not belonging to this particular theory into a common constant. Finally constant elimination must be applied in order to solve cyclic unification problems like 〈x=f(x)〉. The algorithm shows that a combination of finitary unifying regular theories, of Boolean rings, of Abelian groups or of theories of Hullot-type is of unification-type finitary, since these theories have finitary constant-elimination problems. As a special case, unification in a combination of a free Boolean ring with free function symbols is decidable and finitary; the same holds for Abelian groups. Remarkably, it can be shown that unification problems can be solved in the general case E1+... +En if for every i there is a method to solve unification problems in a combination of Ei with free function symbols. Thus, unification in a combination with free function symbols is the really hard case. This paper presents solutions to the important open questions of combining unification algorithms in a disjoint combination of theories. As a special case it provides a solution to the unification of general terms (i.e. terms, where free function symbols are permitted) in Abelian groups and Boolean rings. It extends the known results on unification in a combination of regular and collapse-free theories in two aspects: Arbitrary theories are admissable and we can use complete unification procedures (including universal unification procedures such as narrowing) that may produce an infinite complete set of unifiers for a special theory.