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 formalisation 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 paper explains the idea in as concrete a way as possible and
gives a new derivation within higher-order logic of principles of
α-structural recursion and induction for
$\alpha$-equivalence classes from the ordinary versions of these
principles for abstract syntax trees.
Last modified: Fri Aug 19 20:05:14 BST 2005