Higher-Order Pattern Anti-Unification in Linear Time

被引：8
|
作者：
Baumgartner, Alexander [1 ]
Kutsia, Temur [1 ]
Levy, Jordi [2 ]
Villaret, Mateu [3 ]
机构：
[1] Johannes Kepler Univ Linz, RISC, Linz, Austria
[2] Spanish Council Sci Res CSIC, Artificial Intelligence Res Inst IIIA, Barcelona, Spain
[3] Univ Girona UdG, Dept Informat & Matemat Aplicada IMA, Girona, Spain
来源：
JOURNAL OF AUTOMATED REASONING | 2017年 / 58卷 / 02期
基金：
奥地利科学基金会;
关键词：
Generalizations of lambda terms; Anti-unification; Higher-order patterns; UNIFICATION; TERMS;
D O I：
10.1007/s10817-016-9383-3
中图分类号：
TP18 [人工智能理论];
学科分类号：
081104 ; 0812 ; 0835 ; 1405 ;
摘要：
We present a rule-based Huet's style anti-unification algorithm for simply typed lambda-terms, which computes a least general higher-order pattern generalization. For a pair of arbitrary terms of the same type, such a generalization always exists and is unique modulo -equivalence and variable renaming. With a minor modification, the algorithm works for untyped lambda-terms as well. The time complexity of both algorithms is linear.
引用
收藏
页码：293 / 310
页数：18
相关论文
共 50 条
  • [1] Higher-Order Pattern Anti-Unification in Linear Time
    Alexander Baumgartner
    Temur Kutsia
    Jordi Levy
    Mateu Villaret
    [J]. Journal of Automated Reasoning, 2017, 58 : 293 - 310
  • [2] Restricted higher-order anti-unification for analogy making
    Krumnack, Ulf
    Schwering, Angela
    Gust, Helmar
    Kiffinberger, Kai-Uwe
    [J]. AI 2007: ADVANCES IN ARTIFICIAL INTELLIGENCE, PROCEEDINGS, 2007, 4830 : 273 - 282
  • [3] Refinements of Restricted Higher-Order Anti-Unification for Heuristic-Driven Theory Projection
    Schmidt, Martin
    Gust, Helmar
    Kuehnberger, Kai-Uwe
    Krumnack, Ulf
    [J]. KI 2011: ADVANCES IN ARTIFICIAL INTELLIGENCE, 2011, 7006 : 289 - 300
  • [4] Unification of higher-order patterns in linear time and space
    Qian, Z
    [J]. JOURNAL OF LOGIC AND COMPUTATION, 1996, 6 (03) : 315 - 341
  • [5] Optimizing higher-order pattern unification
    Pientka, B
    Pfenning, F
    [J]. AUTOMATED DEDUCTION - CADE-19, PROCEEDINGS, 2003, 2741 : 473 - 487
  • [6] Linear higher-order pre-unification
    Cervesato, I
    Pfenning, F
    [J]. 12TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1997, : 422 - 433
  • [7] Functions-as-constructors higher-order unification: extended pattern unification
    Libal, Tomer
    Miller, Dale
    [J]. ANNALS OF MATHEMATICS AND ARTIFICIAL INTELLIGENCE, 2022, 90 (05) : 455 - 479
  • [8] Functions-as-constructors higher-order unification: extended pattern unification
    Tomer Libal
    Dale Miller
    [J]. Annals of Mathematics and Artificial Intelligence, 2022, 90 : 455 - 479
  • [9] Unranked second-order anti-unification
    Baumgartner, Alexander
    Kutsia, Temur
    [J]. INFORMATION AND COMPUTATION, 2017, 255 : 262 - 286
  • [10] Higher-Order Dynamic Pattern Unification for Dependent Types and Records
    Abel, Andreas
    Pientka, Brigitte
    [J]. TYPED LAMBDA CALCULI AND APPLICATIONS, (TLCA 2011), 2011, 6690 : 10 - 26
12345