Nominal Unification from a Higher-Order Perspective

Abstract

Nominal Logic is a version of first-order logic with equality, name-binding, renaming via name-swapping and freshness of names. Contrarily to higher-order logic, bindable names, called atoms, and instantiable variables are considered as distinct entities. Moreover, atoms are capturable by instantiations, breaking a fundamental principle of lambda-calculus. Despite these differences, 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 Pattern Unification. This reduction proves that nominal unification can be decided in quadratic deterministic time, using the linear algorithm for Higher-Order Pattern Unification. We also prove that the translation preserves most generality of unifiers.

References in corpus (1)

• Swapping: a natural bridge between named and indexed explicit substitution calculi

Cited by in corpus (9)

• $\alpha$Check: A mechanized metatheory model-checker
• Nominal Unification of Higher Order Expressions with Recursive Let
• Closed nominal rewriting and efficiently computable nominal algebra equality
• Nominal Unification Revisited
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions
• From nominal sets binding to functions and lambda-abstraction: connecting the logic of permutation models with the logic of functions
• Nominal Unification and Matching of Higher Order Expressions with Recursive Let
• Equivariant ZFA and the foundations of nominal techniques
• From nominal to higher-order rewriting and back again