A polynomial nominal unification algorithm

Nominal syntax includes an abstraction operator and a primitive notion of name swapping, that can be used to represent in a simple and natural way systems that include binders. Nominal unification (i.e., solving α-equality constraints between nominal terms) has applications in rewriting and logic programming, amongst others. It is decidable: Urban, Pitts and Gabbay gave a nominal unification algorithm that finds the most general solution to a nominal matching or unification problem, if one exists. A naive implementation of this algorithm is exponential in time; here we describe an algorithm based on a graph representation of nominal terms with lazy propagation of swappings, and show that it is polynomial.