Relating Nominal and Higher-Order Pattern Unification
James Cheney · 2005
Abstract. Higher-order pattern unification and nominal unification are two approaches to unifying modulo some form of α-equivalence (consistent renaming of bound names). The higher-order and nominal approaches seem superficially dissimilar. However, we show that a natural concretion (or name-application) operation for nominal terms can be used to simulate the behavior of higher-order patterns. We describe a form of nominal terms called nominal patterns that includes concretion and for which unification is equivalent to a special case of higher-order pattern unification, and then show that full higher-order pattern unification can be reduced to nominal unification via nominal patterns. 1