The Unification Type of an Equational Theory May Depend on the Instantiation Preorder: From Results for Single Theories to Results for Classes of Theories
Franz Baader, Oliver Fernández Gil
TL;DR
This work analyzes how the choice between restricted and unrestricted instantiation preorders $\le_E^X$ vs $\le_E^V$ affects unification types across equational theories. It provides general meta-results showing when the two preorders yield the same unification type and derives tight (noetherian) upper bounds for broad theory classes, establishing that many regular, locally finite, or restrictive monoidal theories have unrestricted types at most infinitary (and often infinitary), while certain logics like $\mathsf{K}$ can remain zero. It delivers exact unrestricted unification types for several theories, including $\mathsf{ACU}$, $\mathsf{ACUI}$, $\mathsf{ACU}$ and $\mathsf{EL}$, and shows that in some cases the unrestricted type can improve from zero to infinitary when switching preorders. The results illuminate structural criteria—such as Noetherianity and restrictiveness—that guide when preorder choice matters and offer guidance for designing unification procedures in theorem proving and description/modal logics.
Abstract
The unification type of an equational theory is defined using a preorder on substitutions, called the instantiation preorder, whose scope is either restricted to the variables occurring in the unification problem, or unrestricted such that all variables are considered. It has been known for more than three decades that the unification type of an equational theory may vary, depending on which instantiation preorder is used. More precisely, it was shown in 1991 that the theory ACUI of an associative, commutative, and idempotent binary function symbol with a unit is unitary w.r.t. the restricted instantiation preorder, but not unitary w.r.t. the unrestricted one. In 2016 this result was strengthened by showing that the unrestricted type of this theory also cannot be finitary. In the conference version of this article, we considerably improved on this result by proving that ACUI is infinitary w.r.t. the unrestricted instantiation preorder, thus precluding type zero. We also showed that, w.r.t. this preorder, the unification type of ACU (where idempotency is removed from the axioms) and of AC (where additionally the unit is removed) is infinitary, though it is respectively unitary and finitary in the restricted case. In the other direction, we proved (using the example of unification in the description logic EL) that the unification type may actually improve from type zero to infinitary when switching from the restricted instantiation preorder to the unrestricted one. In the present article, we not only determine the unrestricted unification type of considerably more equational theories, but we also prove general results for whole classes of theories. In particular, we show that theories that are regular and finite, regular and locally finite, or regular, monoidal, and satisfy an additional condition are Noetherian, and thus cannot have unrestricted unification type zero.