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
Liste complète des métadonnées

Cited literature [13 references]  Display  Hide  Download

https://hal.inria.fr/hal-00926833
Contributor : Christophe Calvès <>
Submitted on : Friday, January 10, 2014 - 1:27:58 PM
Last modification on : Tuesday, December 18, 2018 - 4:38:25 PM
Document(s) archivé(s) le : Thursday, April 10, 2014 - 10:45:16 PM

File

calves_RTA2013.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

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

Share

Metrics

Record views

141

Files downloads

122