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

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