Alpha-Structural Induction and Recursion for the Lambda Calculus in Constructive Type Theory

摘要

We formulate principles of induction and recursion for a variant of lambda calculus in its original syntax (i.e., with only one sort of names) where α -conversion is based upon name swapping as in nominal abstract syntax. The principles allow to work modulo α -conversion and implement the Barendregt variable convention. We derive them all from the simple structural induction principle on concrete terms and work out applications to some fundamental meta-theoretical results, such as the substitution lemma for α -conversion and the lemma on substitution composition. The whole work is implemented in Agda.