Nominal unification with atom-variables

The problem of nominal unification where variables are allowed for atoms, and computing a complete set of unifiers is considered. The complexity is shown to be NP-complete, while for special cases there are polynomial time algorithms. The main result is a novel algorithm to compute a complete set of unifiers which performs lazy guessing of equality or disequality of atom-variables, runs in NP time, and the collecting variant has more chances to keep the complete set of unifiers small. Applications of this algorithm are in reasoning about program transformations in higher order functional languages. We also present a variant of the unification algorithm that delays guessing and checking solvability, and produces a single most general unifier.