arXivDaily arXiv每日学术速递 周一至周五更新
arXiv 2102.08146cs.LOcs.AI
收藏

带递归 let 的高阶表达式的名义统一与匹配

Nominal Unification and Matching of Higher Order Expressions with Recursive Let

Goethe-Universität Frankfurt（法兰克福歌德大学）；RISC JKU Linz（林茨约翰·开普勒大学符号计算研究所）；IIIA - CSIC（西班牙国家研究委员会人工智能研究所）；Universitat de Girona（赫罗纳大学）

Manfred Schmidt-Schauß, Temur Kutsia, Jordi Levy, Mateu Villaret, Yunus Kutz

备注：
37 pages, 9 figures, This paper is an extended version of the conference publication: Manfred Schmidt-Schauß and Temur Kutsia and Jordi Levy and Mateu Villaret and Yunus Kutz, Nominal Unification of Higher Order Expressions with Recursive Let, LOPSTR-16, Lecture Notes in Computer Science 10184, Springer, p 328 -344, 2016. arXiv admin note: text overlap with arXiv:1608.03771
发表信息：
Fundamenta Informaticae, Volume 185, Issue 3 (May 6, 2022) fi:7191
阅读 PDF
arXiv 页面 ↗HTML 原文 ↗

AI总结：

本文提出带递归 let 的高阶表达式名义统一算法，证明其非确定性多项式时间，并分析多种匹配特化及变量扩展情形的复杂度。

摘要：

本文描述了一种用于带递归 let 的高阶表达式的名义统一的可靠且完备的算法，并证明其运行于非确定性多项式时间。我们还探讨了若干特化情形，例如针对表达式、有向无环图（DAG）以及无垃圾表达式的名义 letrec-匹配，并确定了它们的复杂度。我们还为带递归 let 和原子变量的高阶表达式提供了一种名义统一算法，并证明该算法同样运行于非确定性多项式时间。此外，我们证明了对于带 letrec 和原子变量的名义统一，存在一种猜测策略，该策略在指数增长与非确定性之间进行权衡。针对表示部分 letrec 环境的变量的名义匹配也被证明属于 NP 类。

英文摘要：

A sound and complete algorithm for nominal unification of higher-order expressions with a recursive let is described, and shown to run in nondeterministic polynomial time. We also explore specializations like nominal letrec-matching for expressions, for DAGs, and for garbage-free expressions and determine their complexity. We also provide a nominal unification algorithm for higher-order expressions with recursive let and atom-variables, where we show that it also runs in nondeterministic polynomial time. In addition we prove that there is a guessing strategy for nominal unification with letrec and atom-variable that is a trade-off between exponential growth and non-determinism. Nominal matching with variables representing partial letrec-environments is also shown to be in NP.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

↑