Alpha-structural recursion and induction
Alpha-structural recursion and induction
复制标题
DOI：
10.1145/1147954.1147961
复制
发表时间：
2005-08
期刊：
影响因子：
--
通讯作者：
A. Pitts
中科院分区：
文献类型：
--
作者：
A. Pitts
抽象语法的名义方法通过考虑相对于置换名称不变的结构和性质来处理绑定名称和α-等价问题。排列的使用为抽象语法模α-等价的结构递归和归纳提供了一种常见的、但通常在技术上不正确的、有吸引力的简单形式化。这种方法的核心是有限支持数学对象的概念。本文尽可能具体地解释了这一思想，并从抽象语法树的α-结构递归原理和α-等价类归纳法原理的普通版本出发，在高阶经典逻辑中给出了α-结构递归原理和α-等价类归纳法原理的一个新的推导。
The nominal approach to abstract syntax deals with the issues of bound names and α-equivalence by considering constructions and properties that are invariant with respect to permuting names. The use of permutations gives rise to an attractively simple formalization of common, but often technically incorrect uses of structural recursion and induction for abstract syntax modulo α-equivalence. At the heart of this approach is the notion of finitely supported mathematical objects. This article explains the idea in as concrete a way as possible and gives a new derivation within higher-order classical logic of principles of α-structural recursion and induction for α-equivalence classes from the ordinary versions of these principles for abstract syntax trees.