重新审视名义统一
Nominal Unification Revisited
摘要：
名义统一计算使涉及绑定器的项等于模α等价的替换。虽然名义统一可以被视为等同于米勒的高阶模式统一，但它有一些属性，例如使用带名称的一阶项（与α等价类相反），并且在统一过程中不需要生成新的名称，这使它明显不同于高阶模式统一。本文的目的是简化原论文中关于名义统一的一个繁琐的证明，并对有关名义统一的一些结果进行综述。
英文摘要：
Nominal unification calculates substitutions that make terms involving binders equal modulo alpha-equivalence. Although nominal unification can be seen as equivalent to Miller's higher-order pattern unification, it has properties, such as the use of first-order terms with names (as opposed to alpha-equivalence classes) and that no new names need to be generated during unification, which set it clearly apart from higher-order pattern unification. The purpose of this paper is to simplify a clunky proof from the original paper on nominal unification and to give an overview over some results about nominal unification.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
