License: Creative Commons Attribution 3.0 Unported license (CC BY 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2013.143
URN: urn:nbn:de:0030-drops-40593
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2013/4059/
Go to the corresponding LIPIcs Volume Portal

Calvès, Christophe

Unifying Nominal Unification

pdf-format:
12.pdf (0.5 MB)

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 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.

BibTeX - Entry

@InProceedings{calvs:LIPIcs:2013:4059,
  author =	{Christophe Calv{\`e}s},
  title =	{{Unifying Nominal Unification}},
  booktitle =	{24th International Conference on Rewriting Techniques and Applications (RTA 2013)},
  pages =	{143--157},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-53-8},
  ISSN =	{1868-8969},
  year =	{2013},
  volume =	{21},
  editor =	{Femke van Raamsdonk},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2013/4059},
  URN =		{urn:nbn:de:0030-drops-40593},
  doi =		{10.4230/LIPIcs.RTA.2013.143},
  annote =	{Keywords: unification, nominal, alpha-equivalence, term-graph rewriting}
}

Keywords: unification, nominal, alpha-equivalence, term-graph rewriting
Collection: 24th International Conference on Rewriting Techniques and Applications (RTA 2013)
Issue Date: 2013
Date of publication: 24.06.2013

DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI