Alpha-Structural Recursion and Induction

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, n 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 from the ordinary versions of these principles for abstract syntax trees. Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory—Syntax; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages—Algebraic approaches to semantics; operational semantics; deno...

• Type: Conference
• Year: 2005
• Where: TPHOL
• Authors: Andrew M. Pitts
• Keywords: Abstract Syntax, Abstract Syntax Modulo, Abstract Syntax Trees, Artificial Intelligence, TPHOL 2005