Koji Nakazawa (Nagoya)

Compositional Z: Confluence Proofs for Permutative Conversion

We give new confluence proofs for several lambda calculi with
permutation-like reduction, including lambda calculi with
disjunction and permutative conversions, and a lambda calculus
with explicit substitution. For permutative conversions, naive
parallel reduction technique does not work, and we show that the
difficulties can be avoided by extending the technique proposed by
Dehornoy and van Oostrom, called the Z theorem: existence of a
mapping on terms with the Z property concludes the confluence.