Structural Induction and the lambda-Calculus

                    Rene Vestergaard


We consider formal provability with structural induction and
related proof principles in the lambda-calculus presented with
first-order abstract syntax over one-sorted variable names. As
well as summarising and elaborating on earlier, formally verified
proofs (in Isabelle/HOL) of the relative renaming-freeness of
beta-residual theory and beta-confluence, we also present proofs
of eta-confluence, beta,eta-confluence, the strong weakly-finite
beta-development (aka residual-completion) property, residual
beta-confluence, eta-over-beta-postponement, and notably
beta-standardisation. In the latter case, the known proofs fail in
instructive ways. Interestingly, our uniform proof methodology,
which has relevance beyond the lambda-calculus, properly contains
pen-and-paper proof practices in a precise sense. The proof
methodology also makes precise what is the full algebraic proof
burden of the considered results, which we, moreover, appear to be
the first to resolve.