Unifying Nominal Unification

Author Christophe Calvès

Thumbnail PDF


  • Filesize: 0.49 MB
  • 15 pages

Document Identifiers

Author Details

Christophe Calvès

Cite AsGet BibTex

Christophe Calvès. Unifying Nominal Unification. In 24th International Conference on Rewriting Techniques and Applications (RTA 2013). Leibniz International Proceedings in Informatics (LIPIcs), Volume 21, pp. 143-157, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2013)


Nominal unification is proven to be quadratic in time and space. It was so by two different approaches, both inspired by the Paterson-Wegman linear unification algorithm, but dramatically different in the way nominal and first-order constraints are dealt with. To handle nominal constraints, Levy and Villaret introduced the notion of replacing while Calves and Fernandez use permutations and sets of atoms. To deal with structural constraints, the former use multi-equations in a way similar to the Martelli-Montanari algorithm while the later mimic Paterson-Wegman. In this paper we abstract over these two approaches and genralize them into the notion of modality, highlighting the general ideas behind nominal unification. We show that replacings and environments are in fact isomorphic. This isomorphism is of prime importance to prove intricate properties on both sides and a step further to the real complexity of nominal unification.
  • unification
  • nominal
  • alpha-equivalence
  • term-graph rewriting


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail