Publications

Nominal Unification from a Higher-Order Perspective

Publication Type:

Conference Paper

Authors:

Jordi Levy; Mateu Villaret

Source:

Proc. of the 19th International Conference on Rewriting Techniques and Applications, RTA'08, Springer, Volume 5117, Hagenberg, Austria, p.246-260 (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. We also prove the existence of a most general unifier for solvable instances.

Projects: 
MULOG 2
»