作为 epi-递归器的名义递归器：扩展技术报告
计算机科学中的逻辑
2023-11-15 v2
摘要
我们研究文献中关于带绑定语法的名义递归器，并比较其表达力。术语“名义的”指这些递归器操作于一种语法表示，其中绑定变量的名称显式出现，如在名义逻辑中。我们主张名义递归器可视为 epi-递归器，该概念抽象地捕获了实际递归于其上的构造子与进一步支撑递归的其他算子和性质之间的区别。我们发展了一个用于比较 epi-递归器的抽象框架，并将其实例化到现有名义递归器，以及由它们交叉授粉得到的若干递归器。所得的表达力层级依赖于我们执行此比较的严格程度，并带来对不同语法公理化的相对优点的洞察。我们还将我们的方法学应用于生成名义协递归器的表达力层级，它们是用于定义面向无穷非良基项（其构成如 B"ohm 树等 λ-演算语义概念的基础）的函数的原理。我们的结果用 Isabelle/HOL 定理证明器进行了验证。
引用
@article{arxiv.2301.00894,
title = {Nominal Recursors as Epi-Recursors: Extended Technical Report},
author = {Andrei Popescu},
journal= {arXiv preprint arXiv:2301.00894},
year = {2023}
}