图式句法统一的一个特例
A Special Case of Schematic Syntactic Unification
摘要：
我们提出了一个统一问题的基础上，一阶语法统一，问是否每一个问题的统一问题的一个模式定义的序列是统一的，所谓的循环统一。或者，我们的问题可能被制定为一个递归的过程，调用一阶语法统一的某些绑定发生在解决的形式产生的统一。循环统一与窄化密切相关，因为图式结构可以被视为统一过程中应用的重写规则，而原始语法，因为我们处理递归项结构。然而，循环统一放宽了对变量的限制，因为新的和使用过的额外变量可能会通过重写引入。在这项工作中，我们考虑一个重要的特殊情况下，所谓的半环统一。我们提供了一个充分的条件unifiability的整个序列的结构的基础上，一个足够长的初始段。这仍然是一个悬而未决的问题，这个条件是否也是必要的半圈统一，以及如何可以扩展到循环统一。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
