An Efficient Nominal Unification Algorithm

Jordi Levy & Mateu Villaret
Nominal Unification is an extension of first-order unification where terms can contain binders and unification is performed modulo alpha-equivalence. Here we prove that the existence of nominal unifiers can be decided in quadratic time. First, we linearly-reduce nominal unification problems to a sequence of freshness and equalities between atoms, modulo a permutation, using ideas as Paterson and Wegman for first-order unification. Second, we prove that solvability of these reduced problems may be checked in quadratic...
This data repository is not currently reporting usage information. For information on how your repository can submit usage information, please see our documentation.