TitleNominal Unification from a Higher-Order Perspective
Publication TypeConference Paper
Year of Publication2008
AuthorsLevy J, Villaret M
EditorVoronkov A.
Conference NameProc. of the 19th International Conference on Rewriting Techniques and Applications, RTA'08
Conference LocationHagenberg, Austria

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.