Nominal Unification from a Higher-Order Perspective

TL;DR

This paper demonstrates that nominal unification can be effectively reduced to higher-order pattern unification, enabling efficient decision procedures and preserving unifier generality, thus bridging nominal logic and higher-order logic perspectives.

Contribution

It introduces a reduction from nominal unification to higher-order pattern unification, establishing decidability and efficiency results while maintaining unifier generality.

Findings

Nominal unification reduces to higher-order pattern unification.

Decidability in quadratic deterministic time using existing algorithms.

Translation preserves most general unifiers.

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.