面向含绑定语法的高产集与基于重命名的递归

我引入了重命名富集集（简称 renset），其为公理化含绑定语法上重命名（亦称变量对变量替换）基本性质的代数结构。Renset 在某些方面优于基于 nominal 集的著名基础。特别地，重命名是比 nominal 交换算子更基本的算子，且与变量新鲜度谓词具有更简单的、由等式表达的关系。结合匹配语法构造子性质的一些自然公理，renset 将 lambda 演算项作为抽象数据类型给出了真正极简的刻画——该刻画涉及递归可枚举的无条件等式集，仅引用最基本的项算子：构造子与重命名。此刻画给出了一个递归原理，其（类似于 nominal 集的情况）可通过纳入 Barendregt 变量约定而改进。在将语法解释到语义域时，我的基于重命名的递归器比 nominal 递归器更易部署。我的结果已通过证明助手 Isabelle/HOL 验证。