Induction principles as the foundation of the theory of normalisation: Concepts and Techniques
Résumé
This technical report presents a constructive theory of normalisation based on induction principles, using second-order quantification. Standard techniques are established constructively, such as proving strong normalisation by (possibly non-deterministic) simulation, the termination of lexicographic reductions and multi-set reductions. Two new techniques are then presented to derive strong normalisation: the first one applies to any rewrite system but is classical, the second one applies more specifically to lambda-calculi, especially with explicit substitutions, and is still intuitionistic. The former gives short proofs of PSN for lambda x and lambda bar, the latter gives a proof of PSN for lambdalxr, which is a new result.