Nominal unification
Nominal unification
复制标题
DOI：
10.1016/j.tcs.2004.06.016
复制
发表时间：
2004-09-14
影响因子：
1.1
通讯作者：
Gabbay, MJ
中科院分区：
文献类型：
--
作者：
Urban, C;Pitts, AM;Gabbay, MJ
我们将一阶统一的概括性概括为涉及约束操作的术语之间的实际方程情况。术语的替代变量可以解决该方程式，如果它使等同的术语alpha等效词，即等于重命名的绑定名称。对于我们想到的应用，我们必须考虑简单的替代形式，在替代者替代者的范围内可以捕获以术语来捕获的名称。我们能够采用一种“名义”方法来进行绑定，其中有限的实体被明确命名（而不是使用无名，de bruijn式表示），但获得了这种替代形式的版本，尊重alpha-querativalence并具有良好的算法特性。我们通过调整两个现有想法来实现这一目标。第一个是涉及名称名称的明确替换的术语，除了我们仅使用显式排列（Bioxtive替代）。第二个是统一算法不仅应解决方程问题，而且还应解决名称新鲜度的问题。对这种环境的经典一阶统一问题的简单概括，它保留了后者的宜人属性：涉及α等效性和新鲜度的统一问题是可以决定的；可解决的问题具有大多数通用解决方案。 （c）2004 Elsevier B.V.保留所有权利。
We present a generalisation of first-order unification to the practically important case of equations between terms involving binding operations. A substitution of terms for variables solves such an equation if it makes the equated terms alpha-equivalent, i.e. equal up to renaming bound names. For the applications we have in mind, we must consider the simple, textual form of substitution in which names occurring in terms may be captured within the scope of binders upon substitution. We are able to take a "nominal" approach to binding in which bound entities are explicitly named (rather than using nameless, de Bruijn-style representations) and yet get a version of this form of substitution that respects alpha-equivalence and possesses good algorithmic properties. We achieve this by adapting two existing ideas. The first one is terms involving explicit substitutions of names for names, except that here we only use explicit permutations (bijective substitutions). The second one is that the unification algorithm should solve not only equational problems, but also problems about the freshness of names for terms. There is a simple generalisation of classical first-order unification problems to this setting which retains the latter's pleasant properties: unification problems involving alpha-equivalence and freshness are decidable; and solvable problems possess most general solutions. (C) 2004 Elsevier B.V. All rights reserved.