论文标题
示意性句法统一的特殊情况
A Special Case of Schematic Syntactic Unification
论文作者
论文摘要
我们提出了一个基于一阶句法统一的统一问题，该问题询问示意图定义的统一问题中的每个问题是否是纯粹的，所谓的循环统一。另外，我们的问题可以作为递归程序提出，以统一形式的某些绑定，称为一阶句法统一。循环统一与变窄密切相关，因为示意图构造可以看作是在统一期间应用的重写规则，而原始语法则是我们处理递归术语构造时的原始语法。但是，循环统一放宽了对变量的限制，因为可以通过重写引入新鲜和使用的额外变量。在这项工作中，我们考虑了一个重要的特殊情况，即所谓的半统一。我们根据足够长的初始段的结构为整个序列提供了足够的条件。这仍然是一个悬而未决的问题，是否还需要对半统一的统一以及如何将其扩展到循环统一。
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.
