A polynomial nominal unification algorithm

被引：23
|
作者：
Calves, Christophe [1 ]
Fernandez, Maribel [1 ]
机构：
[1] Kings Coll London, Dept Comp Sci, London WC2R 2LS, England
来源：
THEORETICAL COMPUTER SCIENCE | 2008年 / 403卷 / 2-3期
基金：
英国工程与自然科学研究理事会;
关键词：
binders; alpha-equivalence; nominal syntax; graphs; unification;
D O I：
10.1016/j.tcs.2008.05.012
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Nominal syntax includes an abstraction operator and a primitive notion of name swapping, that can be used to represent in a simple and natural way systems that include binders. Nominal unification (i.e., solving a-equality constraints between nominal terms) has applications in rewriting and logic programming, amongst others. It is decidable: Urban, Pitts and Gabbay gave a nominal unification algorithm that finds the most general solution to a nominal matching or unification problem, if one exists. A naive implementation of this algorithm is exponential in time; here we describe an algorithm based on a graph representation of nominal terms with lazy propagation of swappings, and show that it is polynomial. (C) 2008 Elsevier B.V. All rights reserved.
引用
收藏
页码：285 / 306
页数：22
相关论文
共 50 条
  • [21] AN EFFICIENT UNIFICATION ALGORITHM
    MARTELLI, A
    MONTANARI, U
    ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS, 1982, 4 (02): : 258 - 282
  • [22] A CATEGORICAL UNIFICATION ALGORITHM
    RYDEHEARD, DE
    BURSTALL, RM
    LECTURE NOTES IN COMPUTER SCIENCE, 1986, 240 : 493 - 505
  • [23] An algorithm for distributive unification
    SchmidtSchauss, M
    REWRITING TECHNIQUES AND APPLICATIONS, 1996, 1103 : 287 - 301
  • [24] A PRACTICAL UNIFICATION ALGORITHM
    PURDOM, PW
    INFORMATION SCIENCES, 1991, 55 (1-3) : 123 - 127
  • [25] Unification algorithms cannot be combined in polynomial time
    Hermann, M
    Kolaitis, PG
    INFORMATION AND COMPUTATION, 2000, 162 (1-2) : 24 - 42
  • [26] Towards Fast Nominal Anti-unification of Letrec-Expressions
    Schmidt-Schauss, Manfred
    Nantes-Sobrinho, Daniele
    AUTOMATED DEDUCTION, CADE 29, 2023, 14132 : 456 - 473
  • [27] A Formalisation of Nominal C-Matching through Unification with Protected Variables
    Ayala-Rincon, Mauricio
    de Carvalho-Segundo, Washington
    Fernandez, Maribel
    Nantes-Sobrinho, Daniele
    ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2019, 344 : 47 - 65
  • [28] Meta-variables as infinite lists in nominal terms unification and rewriting
    Gabbay, Murdoch J.
    LOGIC JOURNAL OF THE IGPL, 2012, 20 (06) : 967 - 1000
  • [29] Unification of Multichannel Motion Feature Using Boolean Polynomial
    Ohnishi, Naoya
    Imiya, Atsushi
    Sakai, Tomoya
    ADVANCES IN VISUAL COMPUTING, PT 2, PROCEEDINGS, 2009, 5876 : 807 - +
  • [30] One Context Unification Problems Solvable in Polynomial Time
    Gascon, Adria
    Tiwari, Ashish
    Schmidt-Schauss, Manfred
    2015 30TH ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2015, : 499 - 510
12345