Skip to Main content Skip to Navigation
New interface
Conference papers

Unifying Nominal Unification

Christophe Calvès 1 
1 PAREO - Formal islands: foundations and applications
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : 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 Calvès and Fernández use permutations and sets of atoms. To deal with structural constraints, the former use multi-equation 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [13 references]  Display  Hide  Download
Contributor : Christophe Calvès Connect in order to contact the contributor
Submitted on : Friday, January 10, 2014 - 1:27:58 PM
Last modification on : Wednesday, February 2, 2022 - 4:45:19 PM
Long-term archiving on: : Thursday, April 10, 2014 - 10:45:16 PM


Files produced by the author(s)




Christophe Calvès. Unifying Nominal Unification. RTA 2013 - 24th International Conference on Rewriting Techniques and Applications, Eindhoven University of Technology, Jun 2013, Eindhoven, Netherlands. pp.143-157, ⟨10.4230/LIPIcs.RTA.2013.143⟩. ⟨hal-00926833⟩



Record views


Files downloads