论文标题
与绑定的语法基于生命的和基于重命名的递归
Rensets and Renaming-Based Recursion for Syntax with Bindings
论文作者
论文摘要
我介绍了重命名的富集集（简短的镜头），它们是代数结构在具有绑定的语法上重命名的基本特性（也称为可变的可变替代）。在某些方面与基于名义集的著名基础相比，遗产比较有利。特别是，重命名是比名义交换操作员更基本的操作员，并且与可变的新鲜度谓词具有更简单，方程式的关系。再加上句法构造函数的一些自然公理匹配特性，镜头产生了兰巴达 - 钙符号项作为抽象数据类型的真正简约的表征 - 一种涉及递归枚举的无条件方程组，仅引用了最基本的术语运算符：结构仪和重新品牌。该表征产生了递归原理，该原理（与名义集的情况相似）可以通过合并Barendregt的可变惯例来改进。在语义域中解释语法时，我的基于重命名的递归比名义递归更容易部署。我的结果已通过证明助手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.
