Confluence Proofs of Lambda-Mu-Calculi by Z Theorem

This paper applies Dehornoy et al.’s Z theorem and its variant, called the compositional Z theorem, to prove confluence of Parigot’s $$\lambda \mu $$ -calculi extended by the simplification rules. First, it is proved that Baba et al.’s modified complete developments for the call-by-name and the call-by-value variants of the $$\lambda \mu $$ -calculus with the renaming rule, which is one of the simplification rules, satisfy the Z property. It gives new confluence proofs for them by the Z theorem. Secondly, it is shown that the compositional Z theorem can be applied to prove confluence of the call-by-name and the call-by-value $$\lambda \mu $$ -calculi with both simplification rules, the renaming and the $$\mu \eta $$ -rules, whereas it is hard to apply the ordinary parallel reduction technique or the original Z theorem by one-pass definition of mappings for these variants.