Back to Search
Start Over
Nominal Unification from a Higher-Order Perspective.
- Source :
- Rewriting Techniques & Applications (9783540705888); 2008, p246-260, 15p
- Publication Year :
- 2008
-
Abstract
- Nominal Logic is an extension of first-order logic with equality, name-binding, name-swapping, and freshness of names. Contrarily to higher-order logic, bound variables are treated as atoms, and only free variables are proper unknowns in nominal unification. This allows ˵variable capture″, breaking a fundamental principle of lambda-calculus. Despite this difference, nominal unification can be seen from a higher-order perspective. From this view, we show that nominal unification can be reduced to a particular fragment of higher-order unification problems: higher-order patterns unification. This reduction proves that nominal unification can be decided in quadratic deterministic time. [ABSTRACT FROM AUTHOR]
Details
- Language :
- English
- ISBNs :
- 9783540705888
- Database :
- Complementary Index
- Journal :
- Rewriting Techniques & Applications (9783540705888)
- Publication Type :
- Book
- Accession number :
- 76722542
- Full Text :
- https://doi.org/10.1007/978-3-540-70590-1_17