Nominal Unification from a Higher-Order Perspective

作者：Levy Jordi^*; Villaret Mateu

来源：ACM Transactions on Computational Logic, 2012, 13(2): 10.

DOI：10.1145/2159531.2159532

• Algorithms
• Languages
• Theory
• Higher-order pattern unification
• nominal unification
• Lambda-calculus

Nominal logic is an extension of first-order logic with equality, name-binding, renaming via name-swapping and freshness of names. Contrarily to lambda-terms, in nominal terms, bindable names, called atoms, and instantiable variables are considered as distinct entities. Moreover, atoms are capturable by instantiations, breaking a fundamental principle of the lambda-calculus. Despite these differences, nominal unification can be seen from a higher-order perspective. From this view, we show that nominal unification can be quadratically reduced to a particular fragment of higher-order unification problems: higher-order pattern unification. We also prove that the translation preserves most generality of unifiers.

• 出版日期2012-4