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.

• Type: Journal
• Year: 2010
• Where: CORR
• Authors: Jordi Levy, Mateu Villaret
• Keywords: CORR 2010, Education, Logic, Nominal Logic, Nominal Unification