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.