A FAITHFUL AND QUANTITATIVE NOTION OF DISTANT REDUCTION FOR THE LAMBDA-CALCULUS WITH GENERALIZED APPLICATIONS

. We introduce a call-by-name lambda-calculus AJn with generalized applications which is equipped with distant reduction. This allows to unblock beta-redexes without resorting to the standard permutative conversions of generalized applications used in the original Lambda 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 AJn relates to explicit substitution calculi by means of a faithful translation, in the sense that it preserves strong normalization. Moreover, our calculus AJn and the original Lambda J-calculus determine equivalent notions of strong normalization. As a consequence, Lambda J inherits a faithful translation into explicit substitutions, and its strong normalization can also be characterized by the quantitative typing system designed for AJn, despite the fact that quantitative subject reduction fails for permutative conversions.