文章基本信息

标题：An Efficient Nominal Unification Algorithm
本地全文：下载
作者：Jordi Levy ; Mateu Villaret
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2010
卷号：6
页码：209-226
DOI：10.4230/LIPIcs.RTA.2010.209
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：Nominal logic; unification