We study nominal recursors from the literature on syntax with bindings and compare them with respect to expressiveness. The term "nominal" refers to the fact that these recursors operate on a syntax representation where the names of bound variables appear explicitly, as in nominal logic. We argue that nominal recursors can be viewed as epi-recursors, a concept that captures abstractly the distinction between the constructors on which one actually recurses, and other operators and properties that further underpin recursion.We develop an abstract framework for comparing epi-recursors and instantiate it to the existing nominal recursors, and also to several recursors obtained from them by cross-pollination. The resulted expressiveness hierarchies depend on how strictly we perform this comparison, and bring insight into the relative merits of different axiomatizations of syntax. We also apply our methodology to produce an expressiveness hierarchy of nominal corecursors, which are principles for defining functions targeting infinitary non-well-founded terms (which underlie lambda-calculus semantics concepts such as B\"ohm trees). Our results are validated with the Isabelle/HOL theorem prover.

翻译：摘要：我们研究了语法绑定相关文献中的名义递归子，并比较了它们在表达能力上的差异。术语“名义”指这些递归子作用于一种语法表示，其中绑定变量的名称显式出现（如名义逻辑中的情况）。我们论证了名义递归子可视为广义递归子——这一概念抽象地捕捉了实际递归所基于的构造子（构造函数）与进一步支撑递归的其他算子及性质之间的区别。我们开发了一个用于比较广义递归子的抽象框架，并将其实例化到现有名义递归子中，以及通过交叉融合从它们衍生出的若干递归子。由此产生的表达能力层级取决于我们执行这种比较的严格程度，并揭示了不同语法公理化的相对优势。我们还应用该方法生成了名义共递归子的表达能力层级，这是一种针对无穷非良基项（构成λ-演算语义概念如Böhm树的基础）的函数定义原则。我们的结果已通过Isabelle/HOL定理证明器验证。