Back to Search
Start Over
Nominal unification from a higher-order perspective
- Publication Year :
- 2012
-
Abstract
- Nominal logic is an extension of first-order logic with equality, name-binding, renaming via name-swapping and freshness of names. Contrarily to lambda-terms, in nominal terms, bindable names, called atoms, and instantiable variables are considered as distinct entities. Moreover, atoms are capturable by instantiations, breaking a fundamental principle of the lambda-calculus. Despite these differences, nominal unification can be seen from a higher-order perspective. From this view, we show that nominal unification can be quadratically reduced to a particular fragment of higher-order unification problems: higher-order pattern unification. We also prove that the translation preserves most generality of unifiers. © 2012 ACM 1529-3785/2012/04-ART10 $10.00.
Details
- Database :
- OAIster
- Notes :
- English
- Publication Type :
- Electronic Resource
- Accession number :
- edsoai.on1104785030
- Document Type :
- Electronic Resource