A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications

We introduce a call-by-name lambda-calculus $\lambda Jn$ with generalizedapplications which is equipped with distant reduction. This allows to unblock$\beta$-redexes without resorting to the standard permutative conversions ofgeneralized applications used in the original $\Lambda J$-calculus withgeneralized applications of Joachimski and Matthes. We show strongnormalization of simply-typed terms, and we then fully characterize strongnormalization by means of a quantitative (i.e. non-idempotent intersection)typing system. This characterization uses a non-trivial inductive definition ofstrong normalization --related to others in the literature--, which is based ona weak-head normalizing strategy. We also show that our calculus $\lambda Jn$relates to explicit substitution calculi by means of a faithful translation, inthe sense that it preserves strong normalization. Moreover, our calculus$\lambda Jn$ and the original $\Lambda J$-calculus determine equivalent notionsof strong normalization. As a consequence, $\lambda J$ inherits a faithfultranslation into explicit substitutions, and its strong normalization can alsobe characterized by the quantitative typing system designed for $\lambda Jn$,despite the fact that quantitative subject reduction fails for permutativeconversions.