- Abstract:
-
Higher-order pattern unification and nominal unification are two approaches to unifying modulo some form of alpha-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.
- Links To Paper
- Local copy
- Online proceedings
- Bibtex format
- @InProceedings{EDI-INF-RR-0320,
- author = {
James Cheney
},
- title = {Relating Nominal and Higher-Order Pattern Unification},
- book title = {Proc. UNIF 2005},
- year = 2005,
- month = {Apr},
- url = {http://homepages.inf.ed.ac.uk/jcheney/publications/hopu-nu.pdf},
- }
|
