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 prop 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 strict we perform this comparison, and bring insight into the relative merits of different axiomatizations of syntax. Our results are validated with the Isabelle/HOL theorem prover.

翻译：我们从关于语法的文献中用约束物研究名义递归器,并在表达性方面比较它们。“名义”一词是指这些递解器在语法代表法中运行,其中约束变量的名称明显可见,就像名义逻辑一样。我们争辩说,名义递解器可以被视为上层递解器,这个概念抽象地捕捉了实际递解的构建器与其他操作器和特性之间的区分,进一步循环。我们开发了一个抽象框架,用来比较上层递解器并将其与现有的名义递解器进行即时比较,并同时通过交叉极化从它们获得若干递解器。结果的表态等级取决于我们进行这种比较的严格程度,并洞察到不同语法的分解法的相对优点。我们的结果通过伊莎贝尔/HOL 理论验证来验证。