Unification of higher-order patterns in linear time and space

被引：13
|
作者：
Qian, Z [1 ]
机构：
[1] UNIV BREMEN,FB INFORMAT 3,BREMEN,GERMANY
来源：
JOURNAL OF LOGIC AND COMPUTATION | 1996年 / 6卷 / 03期
关键词：
higher-order unification; complexity of unification;
D O I：
10.1093/logcom/6.3.315
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
Higher-order patterns are simply typed X-terms in long beta-normal form where the arguments of a free variable are always eta-equal to distinct bound variables. It has been proved that unification of higher-order patterns module alpha, beta and eta reductions in the simply typed lambda-calculus is decidable and unifiable higher-order patterns have a most general unifier. In this paper a unification algorithm for higher-order patterns is presented, whose time and space complexities are proved to be linear in the size of input.
引用
收藏
页码：315 / 341
页数：27
相关论文
共 50 条
  • [31] Eliminating redundancy in higher-order unification: A lightweight approach
    Pientka, Brigitte
    AUTOMATED REASONING, PROCEEDINGS, 2006, 4130 : 362 - 376
  • [32] Managing structural information by higher-order colored unification
    Hutter, Dieter, 1600, Kluwer Academic Publishers, Dordrecht, Netherlands (25):
  • [33] A SPACE/TIME TRADEOFF METHODOLOGY USING HIGHER-ORDER FUNCTIONS
    Wester, Rinse
    Kuper, Jan
    2013 23RD INTERNATIONAL CONFERENCE ON FIELD PROGRAMMABLE LOGIC AND APPLICATIONS (FPL 2013) PROCEEDINGS, 2013,
  • [34] Formalization of Linear Space Theory in the Higher-Order Logic Proving System
    Zhang, Jie
    Mao, Danwen
    Guan, Yong
    JOURNAL OF APPLIED MATHEMATICS, 2013,
  • [35] Moire fringes of higher-order harmonics versus higher-order moire patterns
    Yeganeh, Mohammad
    Rasouli, Saifollah
    APPLIED OPTICS, 2018, 57 (33) : 9777 - 9788
  • [36] Higher-order being and time
    Skiba, Lukas
    NOUS, 2024,
  • [37] The geometry of linear higher-order recursion
    Dal Lago, U
    LICS 2005: 20th Annual IEEE Symposium on Logic in Computer Science - Proceedings, 2005, : 366 - 375
  • [38] Higher-order linear lossless systems
    Rao, S.
    Rapisarda, P.
    INTERNATIONAL JOURNAL OF CONTROL, 2008, 81 (10) : 1519 - 1536
  • [39] The Geometry of Linear Higher-Order Recursion
    Dal Lago, Ugo
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2009, 10 (02)
  • [40] Higher-order linear ramified recurrence
    Dal Lago, U
    Martini, S
    Roversi, L
    TYPES FOR PROOFS AND PROGRAMS, 2004, 3085 : 178 - 193
12345