Confluence and Strong Normalisation of the Generalised Multiary λ-Calculus

Abstract

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