Higher-order pattern unification and nominal unification are two approaches to unifying modulo some form of #-equivalence (consistent renaming of bound names). Though the higher-order and nominal approaches superficially dissimilar, there is a natural concretion (or name-application) operation for nominal terms that 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 how full higher-order pattern unification can be reduced to nominal unification via nominal patterns.
|Title of host publication||Proceedings of UNIF 2005|
|Number of pages||16|
|Publication status||Published - 2005|