We present a unification problem based on first-order syntactic unification which ask whether every problem in a schematically-defined sequence of unification problems is unifiable, so called loop unification. Alternatively, our problem may be formulated as a recursive procedure calling first-order syntactic unification on certain bindings occurring in the solved form resulting from unification. Loop unification is closely related to Narrowing as the schematic constructions can be seen as a rewrite rule applied during unification, and primal grammars, as we deal with recursive term constructions. However, loop unification relaxes the restrictions put on variables as fresh as well as used extra variables may be introduced by rewriting. In this work we consider an important special case, so called semiloop unification. We provide a sufficient condition for unifiability of the entire sequence based on the structure of a sufficiently long initial segment. It remains an open question whether this condition is also necessary for semiloop unification and how it may be extended to loop unification.
翻译:我们提出了基于一阶合成统一的统一问题, 问一问在一阶合成的统一问题中每个问题是否都是无法解决的, 也就是所谓的环状统一。 或者, 我们的问题可以作为一种循环程序来形成, 要求对统一产生的已解决形式中的某些结合物进行一阶合成统一。 环状统一与缩小密切相关, 因为系统构造可以被视为在统一期间应用的重写规则, 和原始语法, 因为我们处理的是重复的术语构造。 但是, 环状统一可以放松对变量的限制, 对新变数和使用的额外变数的限制, 也可以通过重写来引入。 在这项工作中, 我们考虑一个重要的特殊案例, 叫做半环状统一。 我们为基于足够长的初始段结构整个序列的不可调和性提供了充分的条件。 我们对于半圆形统一是否同样需要这一条件, 以及如何将其扩展为循环统一, 仍是一个未决问题。