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 条
12345