05/10/2000: Ralph Matthes, Univ. de Munich---
Parigot's lambda-mu-calculus and inductive types
Résumé
Lambda-mu-calculus essentially is the extension of natural deduction by
"reductio ad absurdum" (RAA), i.e., by a term formation rule corresponding
to stability (not not A -> A, also called "duplex negatio affirmat") and
by rewrite rules for the simplification of the application of elimination
rules to RAA (in the case of -> elimination this corresponds to the fact
that the stability of A->B is derivable from that of B).
In [P], a proof of strong normalization of the second-order
lambda-mu-calculus is given by using reducibility candidates, defined by
an inductive definition (the set of reducibility candidates is the
smallest set of sets of terms, closed under...). In contrast to that, we
will study a notion of reducibility candidates (saturated sets) where the
candidates are individually closed under several operations (which is more
common in the literature). A less common feature: The closure amounts to a
non-strictly positive inductive definition.
The easier construction has a major additional benefit: Led by an informal
understanding of modified realizability, we arrive at a
reduction-preserving embedding of second-order lambda-mu-calculus into
system F, extended by iteration on non-strictly positive inductive types,
which in turn embeds into pure system F (as is well-known). In contrast to
this embedding, the CPS translation considered in [P] maps the RAA redexes
and their contracta to the same term, and hence needs additional arguments
on RAA reductions alone to guarantee strong
normalization of the whole calculus.
The proof by saturated sets immediately extends to sum types with
permutative conversions, whereas we cannot expect this to be true of the
reduction-preserving embedding into system F. Nevertheless, the system
without permutative conversions may again be embedded. This even carries
over to iteration and primitive recursion on inductive types.
To sum up: Suggested by a new candidate-style proof of strong
normalization for second-order lambda-mu-calculus, we even get a
reduction-preserving embedding into system F, which moreover readily
extends to positive concepts such as sums and inductive types. The key
idea is to use non-strictly positive inductive definitions.
[P] Michel Parigot. Proofs of strong normalisation for second order
classical natural deduction, JSL 62(4) 1461-1479, 1997.