Nominal Unification Revisited

TL;DR

This paper revisits nominal unification, clarifying its properties and simplifying foundational proofs, thereby enhancing understanding of its relation to higher-order pattern unification.

Contribution

It simplifies a complex proof from the original nominal unification work and provides an overview of key results, clarifying its unique properties.

Findings

Nominal unification uses first-order terms with names, avoiding new name generation.

It is equivalent to higher-order pattern unification but has distinct properties.

The paper clarifies the theoretical foundations and properties of nominal unification.

Abstract

Nominal unification calculates substitutions that make terms involving binders equal modulo alpha-equivalence. Although nominal unification can be seen as equivalent to Miller's higher-order pattern unification, it has properties, such as the use of first-order terms with names (as opposed to alpha-equivalence classes) and that no new names need to be generated during unification, which set it clearly apart from higher-order pattern unification. The purpose of this paper is to simplify a clunky proof from the original paper on nominal unification and to give an overview over some results about nominal unification.