基于重命名集和重命名递归的绑定搜索算法
Rensets and Renaming-Based Recursion for Syntax with Bindings
摘要：
我介绍了重命名富集集（简称rensets），这是一种代数结构，它公理化了重命名（也称为变量对变量的替换）的基本属性。Rensets在某些方面与基于名义集合的著名基础相比毫不逊色。特别地，重命名是比名义交换操作符更基本的操作符，并且与变量新鲜度谓词具有更简单的等式表达关系。再加上一些自然公理匹配的属性的语法构造器，rensets产生一个真正的最低限度的表征的abstract演算条款作为一个抽象的数据类型-一个涉及一个递归的无条件方程组，只涉及最基本的长期运营商：构造器和重命名。这个特征产生了一个递归原理，它（类似于名义集的情况）可以通过结合巴伦德雷格特的变量约定来改进。当解释语义域中的语法时，我的基于重命名的递归比名义递归更容易部署。我的结果已经过证明助手Isabelle/HOL的验证。
英文摘要：
I introduce renaming-enriched sets (rensets for short), which are algebraic structures axiomatizing fundamental properties of renaming (also known as variable-for-variable substitution) on syntax with bindings. Rensets compare favorably in some respects with the well-known foundation based on nominal sets. In particular, renaming is a more fundamental operator than the nominal swapping operator and enjoys a simpler, equationally expressed relationship with the variable freshness predicate. Together with some natural axioms matching properties of the syntactic constructors, rensets yield a truly minimalistic characterization of lambda-calculus terms as an abstract datatype -- one involving a recursively enumerable set of unconditional equations, referring only to the most fundamental term operators: the constructors and renaming. This characterization yields a recursion principle, which (similarly to the case of nominal sets) can be improved by incorporating Barendregt's variable convention. When interpreting syntax in semantic domains, my renaming-based recursor is easier to deploy than the nominal recursor. My results have been validated with the proof assistant Isabelle/HOL.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
