Ítem


An Efficient Nominal Unification Algorithm

Nominal Unification is an extension of first-order unification where terms can contain binders and unification is performed modulo α 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 quadràtic time. Finally, we point out how using ideas of Brown and Tarjan for unbalanced merging, we could solve these reduced problems more efficiently

Leibniz International Proceedings in Informatics (LIPPICS) : Proceedings of the 21st International Conference on Rewriting Techniques and Applications : RTA 2010 : July 11-13 2010: Edinburgh, Scottland, UK, 2010, vol. 6, p.209-226

Dagstuhl Publishing

Autor: Levy, Jordi
Villaret i Ausellé, Mateu
Data: 2010
Resum: Nominal Unification is an extension of first-order unification where terms can contain binders and unification is performed modulo α 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 quadràtic time. Finally, we point out how using ideas of Brown and Tarjan for unbalanced merging, we could solve these reduced problems more efficiently
Format: application/pdf
ISSN: 1868-8969
Accés al document: http://hdl.handle.net/10256/8404
Llenguatge: eng
Editor: Dagstuhl Publishing
Col·lecció: Reproducció digital del document publicat a: http://dx.doi.org/10.4230/LIPIcs.RTA.2010.209
Articles publicats (D-IMA)
És part de: Leibniz International Proceedings in Informatics (LIPPICS) : Proceedings of the 21st International Conference on Rewriting Techniques and Applications : RTA 2010 : July 11-13 2010: Edinburgh, Scottland, UK, 2010, vol. 6, p.209-226
Drets: Attribution-NonCommercial-NoDerivs 3.0 Spain
URI Drets: http://creativecommons.org/licenses/by-nc-nd/3.0/es/
Matèria: Algorismes computacionals
Computer algorithms
Lògica matemàtica
Logic, Symbolic and mathematical
Complexitat computacional
Computational complexity
Títol: An Efficient Nominal Unification Algorithm
Tipus: info:eu-repo/semantics/article
Repositori: DUGiDocs

Matèries

Autors