一句话：提出 λJn 演算，用远距离归约替代置换转换，以非幂等交类型系统刻画强规范化，并给出到显式替换的忠实翻译。
该文针对带广义应用的 λJ 演算中，β-归约受阻时需借助置换转换的问题，引入按名调用的 λJn 演算，并采用远距离归约直接解除 β-归约式阻塞。作者证明简单类型项强规范化，并用定量（非幂等交）类型系统完整刻画强规范化；该刻画依赖基于弱头规范化策略的归纳定义。文章还给出 λJn 到显式替换演算的忠实翻译，保持强规范化，并证明 λJn 与原 ΛJ 的强规范化概念等价。由此，ΛJ 也获得到显式替换的忠实翻译，并可由为 λJn 设计的定量类型系统刻画其强规范化，尽管置换转换下定量主体归约性质不成立。
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.
@article{paperbot2739,
title = {A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications},
author = {José Espírito Santo and Delia Kesner and Loïc Peyrot},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 3},
year = {2024},
doi = {10.46298/lmcs-20(3:10)2024}
}