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 classical logic of
principles of α-structural recursion and induction
for α-equivalence classes from the ordinary versions of
these principles for abstract syntax trees.