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.

翻译：方程理论的可统一性类型是通过称为实例化预序的替换预序来定义的，其范围要么限于统一问题中出现的变量，要么不受限制地考虑所有变量。三十多年来，人们已经知道方程理论的可统一性类型可能因所使用的实例化预序而异。更具体地说，1991年的研究表明，具有单位元的结合、交换、幂等二元函数符号的理论ACUI在受限实例化预序下是单一的，但在无限制实例化预序下则不是单一的。2016年，这一结果得到加强，证明该理论的无限制类型也不能是有限型的。在本文的会议版本中，我们通过证明ACUI在无限制实例化预序下是无限型的，从而排除了零型，极大地改进了这一结果。我们还表明，相对于该预序，ACU（从公理中移除幂等性）和AC（进一步移除单位元）的可统一性类型是无限型的，尽管它们在受限情况下分别是单一型和有限型的。在另一个方向上，我们证明（使用描述逻辑EL中的统一示例）当从受限实例化预序切换到无限制实例化预序时，可统一性类型实际上可能从零型提升为无限型。在本文中，我们不仅确定了更多方程理论的无限制可统一性类型，而且还证明了整个理论类的一般结果。特别地，我们证明了正则且有限、正则且局部有限，或正则、幺半群且满足附加条件的理论是诺特型的，因此不可能具有无限制可统一性类型零。