Confluence and strong normalisation of the generalised multiary lambda-calculus

Abstract

In a previous work we introduced the {\em generalised multiary $\lambda$-calculus} lambda-Jm, 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 lambda-Jm. Proofs of these results lift corresponding ones obtained by Joachimski and Matthes for the system $\Lambda J$. Such lifting requires the study of how multiarity and some forms of generality can express each other. This study identifies a variant of $\Lambda J$, and another system isomorphic to it, as being the subsystems of lambda-Jm with, respectively, minimal and maximal use of multiarity. We argue then that lambda-Jm is the system with the right use of multiarity.