Sciweavers

CORR
2010
Springer

Nominal Unification from a Higher-Order Perspective

13 years 2 months ago
Nominal Unification from a Higher-Order Perspective
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.
Jordi Levy, Mateu Villaret
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2010
Where CORR
Authors Jordi Levy, Mateu Villaret
Comments (0)