Relating Nominal and Higher-Order Pattern Unification

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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 languageEnglish
Title of host publicationProceedings of UNIF 2005
Pages104-119
Number of pages16
Publication statusPublished - 2005

Cite this