Nominal Unification of Higher Order Expressions with Recursive Let

被引：7
|
作者：
Schmidt-Schauss, Manfred [1 ]
Kutsia, Temur [2 ]
Levy, Jordi [3 ]
Villaret, Mateu [4 ]
机构：
[1] GU Frankfurt, Frankfurt, Germany
[2] JKU Linz, RISC, Linz, Austria
[3] CSIC, IIIA, Barcelona, Spain
[4] Univ Girona, IMA, Girona, Spain
来源：
LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, LOPSTR 2016 | 2017年 / 10184卷
关键词：
Nominal unification; Lambda calculus; Higher-order expressions; Recursive let; Operational semantics; 2ND-ORDER UNIFICATION; ALGORITHM; UNDECIDABILITY;
D O I：
10.1007/978-3-319-63139-4_19
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in non-deterministic polynomial time. We also explore specializations like nominal letrec-matching for plain expressions and for DAGs and determine their complexity.
引用
收藏
页码：328 / 344
页数：17
相关论文
共 50 条
  • [1] Nominal Unification and Matching of Higher Order Expressions with Recursive Let
    Schmidt-Schauss, Manfred
    Kutsia, Temur
    Levy, Jordi
    Villaret, Mateu
    Kutz, Yunus
    FUNDAMENTA INFORMATICAE, 2022, 185 (03) : 247 - 283
  • [2] Nominal unification from a higher-order perspective
    Levy, Jordi
    Villaret, Mateu
    REWRITING TECHNIQUES AND APPLICATIONS, PROCEEDINGS, 2008, 5117 : 246 - +
  • [3] Nominal Unification from a Higher-Order Perspective
    Levy, Jordi
    Villaret, Mateu
    ACM TRANSACTIONS ON COMPUTATIONAL LOGIC, 2012, 13 (02)
  • [4] (Nominal) Unification by Recursive Descent with Triangular Substitutions
    Kumar, Ramana
    Norrish, Michael
    INTERACTIVE THEOREM PROVING, PROCEEDINGS, 2010, 6172 : 51 - 66
  • [5] Unification of Program Expressions with Recursive Bindings
    Schmidt-Schauss, Manfred
    Sabel, David
    PROCEEDINGS OF THE 18TH INTERNATIONAL SYMPOSIUM ON PRINCIPLES AND PRACTICE OF DECLARATIVE PROGRAMMING (PPDP 2016), 2016, : 160 - 173
  • [6] Dynamics and Solutions' Expressions of a Higher-Order Nonlinear Fractional Recursive Sequence
    Alshareef, Abeer
    Alzahrani, Faris
    Khan, Abdul Qadeer
    MATHEMATICAL PROBLEMS IN ENGINEERING, 2021, 2021 (2021)
  • [7] Towards Fast Nominal Anti-unification of Letrec-Expressions
    Schmidt-Schauss, Manfred
    Nantes-Sobrinho, Daniele
    AUTOMATED DEDUCTION, CADE 29, 2023, 14132 : 456 - 473
  • [8] Nominal unification
    Urban, C
    Pitts, AM
    Gabbay, MJ
    THEORETICAL COMPUTER SCIENCE, 2004, 323 (1-3) : 473 - 497
  • [9] Nominal unification
    Urban, C
    Pitts, A
    Gabbay, M
    COMPUTER SCIENCE LOGIC, PROCEEDINGS, 2003, 2803 : 513 - 527
  • [10] Higher order unification and the interpretation of focus
    Pulman, SG
    LINGUISTICS AND PHILOSOPHY, 1997, 20 (01) : 73 - 115
12345