Abstract / Description of output
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.
| Original language | English |
|---|---|
| Title of host publication | Proceedings of UNIF 2005 |
| Pages | 104-119 |
| Number of pages | 16 |
| Publication status | Published - 2005 |