An Efficient Nominal Unification Algorithm

Authors Jordi Levy, Mateu Villaret



PDF
Thumbnail PDF

File

LIPIcs.RTA.2010.209.pdf
  • Filesize: 193 kB
  • 18 pages

Document Identifiers

Author Details

Jordi Levy
Mateu Villaret

Cite AsGet BibTex

Jordi Levy and Mateu Villaret. An Efficient Nominal Unification Algorithm. In Proceedings of the 21st International Conference on Rewriting Techniques and Applications. Leibniz International Proceedings in Informatics (LIPIcs), Volume 6, pp. 209-226, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)
https://doi.org/10.4230/LIPIcs.RTA.2010.209

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.
Keywords
  • Nominal logic
  • unification

Metrics

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

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail