We introduce a call-by-name lambda-calculus $\lambda Jn$ 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 $\lambda Jn$ relates to explicit substitution calculi by means of a faithful translation, in the sense that it preserves strong normalization. Moreover, our calculus $\lambda Jn$ 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 $\lambda Jn$, despite the fact that quantitative subject reduction fails for permutative conversions.

翻译：我们提出一种带广义应用且支持远期归约的按名调用λ演算$\lambda Jn$。该演算无需使用Joachimski与Mathes原始$\Lambda J$演算中处理广义应用的标准置换转换，即可解除$\beta$-可约式。本文证明了简单类型项的强规范化性质，并通过量化（即非幂等交）类型系统完整刻画了强规范化特性。此刻画采用一种与文献中其他定义相关的非平凡归纳定义，其基础是弱头规范化策略。我们还证明$\lambda Jn$演算通过忠实翻译与显式替换演算相关联（保持强规范化意义下）。此外，$\lambda Jn$演算与原始$\Lambda J$演算在强规范化概念上等价。由此推论，$\Lambda J$继承了到显式替换的忠实翻译，且其强规范化性质亦可由为$\lambda Jn$设计的量化类型系统所刻画——尽管置换转换场景下量化主体归约性质失效。