License: Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported license (CC BY-NC-ND 3.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.RTA.2010.209
URN: urn:nbn:de:0030-drops-26544
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2010/2654/
Go to the corresponding LIPIcs Volume Portal

Levy, Jordi ; Villaret, Mateu

An Efficient Nominal Unification Algorithm

pdf-format:
10002.LevyJordi.2654.pdf (0.2 MB)

Abstract

Nominal Unification is an extension of first-order unification where terms can contain binders and unification is performed modulo alpha-equivalence. Here we prove that the existence of nominal unifiers can be decided in quadratic time. First, we linearly-reduce nominal unification problems to a sequence of freshness and equalities between atoms, modulo a permutation, using ideas as Paterson and Wegman for first-order unification. Second, we prove that solvability of these reduced problems may be checked in quadratic time. Finally, we point out how using ideas of Brown and Tarjan for unbalanced merging, we could solve these reduced problems more efficiently.

BibTeX - Entry

@InProceedings{levy_et_al:LIPIcs:2010:2654,
  author =	{Jordi Levy and Mateu Villaret},
  title =	{{An Efficient Nominal Unification Algorithm}},
  booktitle =	{Proceedings of the 21st International Conference on Rewriting Techniques and Applications},
  pages =	{209--226},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-18-7},
  ISSN =	{1868-8969},
  year =	{2010},
  volume =	{6},
  editor =	{Christopher Lynch},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2010/2654},
  URN =		{urn:nbn:de:0030-drops-26544},
  doi =		{10.4230/LIPIcs.RTA.2010.209},
  annote =	{Keywords: Nominal logic, unification}
}

Keywords: Nominal logic, unification
Collection: Proceedings of the 21st International Conference on Rewriting Techniques and Applications
Issue Date: 2010
Date of publication: 06.07.2010

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