带递归let的高阶表达式的名义合一与匹配
计算机科学中的逻辑
2023-06-22 v4 人工智能
摘要
本文描述了一种用于带递归let的高阶表达式的名义合一的可靠且完备的算法，并证明其可在非确定性多项式时间内运行。我们还探讨了针对表达式、DAG以及无垃圾表达式的名义letrec匹配等特化情形，并确定了它们的复杂度。我们还给出了一种用于带递归let和原子变量的高阶表达式的名义合一算法，并证明其同样在非确定性多项式时间内运行。此外，我们证明了针对带letrec和原子变量的名义合一存在一种猜测策略，该策略在指数增长与非确定性之间取得了折衷。我们还证明了表示部分letrec环境的变量的名义匹配也属于NP类。
引用
@article{arxiv.2102.08146,
title = {Nominal Unification and Matching of Higher Order Expressions with Recursive Let},
author = {Manfred Schmidt-Schauß and Temur Kutsia and Jordi Levy and Mateu Villaret and Yunus Kutz},
journal= {arXiv preprint arXiv:2102.08146},
year = {2023}
}
备注
37 pages, 9 figures, This paper is an extended version of the conference publication: Manfred Schmidt-Schau{\ss} 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