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$的按名调用lambda演算，其具有广义应用并配备远距离归约机制。该机制无需使用Joachimski和Matthes原始$\Lambda J$演算中处理广义应用的标准置换转换，即可解除$\beta$可约式。我们证明了简单类型项的强规范化性质，并通过定量（即非幂等交集）类型系统完整刻画了强规范化特征。该刻画采用一种与文献中相关定义相关的非平凡强规范化归纳定义——该定义基于弱头规范化策略。我们还证明了我们的演算$\lambda Jn$可通过忠实翻译（即保持强规范化性质）与显式替换演算建立关联。此外，$\lambda Jn$演算与原始$\Lambda J$演算具有等价的强规范化概念。由此可得，$\lambda J$可继承到显式替换的忠实翻译，且其强规范化性质同样可由专为$\lambda Jn$设计的定量类型系统刻画——尽管置换转换破坏了定量主体归约性质。