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 条

[31] Rewriting with generalized nominal unification
Kutz, Yunus
Schmidt-Schauss, Manfred
MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE, 2020, 30 (06) : 710 - 735
[32] AN EFFICIENT NOMINAL UNIFICATION ALGORITHM
Levy, Jordi
Villaret, Mateu
PROCEEDINGS OF THE 21ST INTERNATIONAL CONFERENCE ON REWRITING TECHNIQUES AND APPLICATIONS (RTA'10), 2010, 6 : 209 - 225
[33] Nominal C-Unification
Ayala-Rincon, Mauricio
De Carvalho-Segundo, Washington
Fernandez, Maribel
Nantes-Sobrinho, Daniele
LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION (LOPSTR 2017), 2018, 10855 : 235 - 251
[34] A polynomial nominal unification algorithm
Calves, Christophe
Fernandez, Maribel
THEORETICAL COMPUTER SCIENCE, 2008, 403 (2-3) : 285 - 306
[35] Higher-order recursive path ordering
Universite de Paris Sud, Orsay, France
Proc Symp Logic Comput Sci, (402-411):
[36] On the global behavior of higher order recursive sequences
Douraki, MJ
Dehghan, M
Razavi, A
APPLIED MATHEMATICS AND COMPUTATION, 2005, 169 (02) : 819 - 831
[37] Adaptive recursive higher order polynomial filter
Fnaiech, F
Sayadi, M
Najim, M
PROCEEDINGS OF THE IEEE-EURASIP WORKSHOP ON NONLINEAR SIGNAL AND IMAGE PROCESSING (NSIP'99), 1999, : 684 - 688
[38] Linear higher-order pre-unification
Cervesato, I
Pfenning, F
12TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 1997, : 422 - 433
[39] HIGHER-ORDER UNIFICATION WITH DEPENDENT FUNCTION TYPES
ELLIOTT, CM
LECTURE NOTES IN COMPUTER SCIENCE, 1989, 355 : 121 - 136
[40] AC-unification of higher-order patterns
Boudet, A
Contejean, E
PRINCIPLES AND PRACTICE OF CONSTRAINT PROGRAMMING - CP 97, 1997, 1330 : 267 - 281

← 1 2 3 4 5 →