Confluence and strong normalisation of the generalised multiary λ-calculus

In a previous work we introduced the generalised multiary lambda-calculus lambdaJ(m), an extension of the lambda-calculus where functions can be applied to lists of arguments (a feature which we call "multiarity") and encompassing "generalised" eliminations of von Plato. In this paper we prove confluence and strong normalisation of the reduction relations of lambdaJ(m). Proofs of these results lift corresponding ones obtained by Joachimski and Matthes for the system LambdaJ. Such lifting requires the study of how multiarity and some forms of generality can express each other. This study identifies a variant of LambdaJ, and another system isomorphic to it, as being the subsystems of lambdaJ(m) with, respectively, minimal and maximal use of multiarity. We argue then that lambdaJ(m) is the system with the right use of multiarity.