The Primitive Proof Theory of the lambda-Calculus

                 Rene Vestergaard


We consider formal provability with structural induction and
related proof principles in the lambda-calculus seen as a
(functional) programming language, i.e., presented with
first-order abstract syntax over one-sorted variable names.
Structural induction is the principal primitive proof principle of
that particular syntactic framework and it is, indeed,
near-ubiquitously employed in informal proofs in the wider
programming-language theory community. In spite of substantial
efforts in the theorem-proving community, these informal proofs
have unfortunately been neither formalised nor considered
formalisable so far. This impasse must naturally raise
uncomfortable questions about the formal validity of the proof
principles.

The highlights of the results we establish formally by structural
means are the relative renaming freeness of beta-residual theory,
decidability of alpha-equivalence, beta-confluence,
eta-confluence, beta,eta-confluence, beta residual completion (aka
strong weakly-finite beta-development), residual beta-confluence,
eta-over-beta postponement, and notably beta-standardisation.
Interestingly, our uniform proof methodology, which has relevance
beyond the lambda-calculus, properly contains pen-and-paper proof
practices in a precise sense except for the cases of
alpha-decidability and beta-standardisation where the known proofs
fail in instructive ways. Our notion of residual completion,
furthermore, presents a simplified treatment of residual theory
compared to established practice, be it for strong finite
development or for Huet's Prism theorem/Levy's Cube lemma.
Overall, our approach makes precise what is the full algebraic
proof burden of the considered results and our proofs, in fact,
appear to be the first complete developments in the literature.

Our results are relevant for researchers in programming language
theory, rewriting, proof theory, and mechanised theorem
proving/automated reasoning.