A faithful and quantitative notion of distant reduction for generalized applications

We introduce a call-by-name lambda-calculus lambdaJ with generalized applications which integrates a notion of distant reduction that allows to unblock beta-redexes without resorting to the permutative conversions of generalized applications. We show strong normalization of simply typed terms, and we then fully characterize strong normalization by means of a quantitative typing system. This characterization uses a non-trivial inductive definition of strong normalization --that we relate to others in the literature--, which is based on a weak-head normalizing strategy. Our calculus relates to explicit substitution calculi by means of a translation between the two formalisms which is faithful, in the sense that it preserves strong normalization. We show that our calculus lambdaJ and the well-know calculus LambdaJ determine equivalent notions of strong normalization. As a consequence, LambdaJ inherits a faithful translation into explicit substitutions, and its strong normalization can be characterized by the quantitative typing system designed for lambdaJ, despite the fact that quantitative subject reduction fails for permutative conversions