Compositional Z: confluence proofs for permutative conversion (Q514511)

The Z-theorem of \textit{P. Dehorney} and \textit{Z. van Oostrom} [``Proving confluence by monotonic single-step upperbound functions'', in: Logical models of reasoning and computation (LMRC-08) (2008)] allows the proof of confluence for a number of variants of the \(\lambda\)-calculus. In the current paper, the authors generalise this to a compositional Z-theorem, which is easily proved from the Z-theorem. The new theorem allows, in addition, proofs of confluence for \(\lambda\)-calculi corresponding to intuitionistic and classical natural deduction with disjunction and permutative conversions as well as a \(\lambda\)-calculus with explicit substitution.