带广义应用的λ演算中远距离归约的一种忠实且定量的概念
A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications
AI总结：
本文提出带广义应用的按名调用λ演算λJn，利用远距离归约避免置换转换，通过定量类型系统完整刻画强正规化，并建立与显式替换演算的忠实翻译关系。
摘要：
我们引入了一个按名调用（call-by-name）的λ演算λJn，它带有广义应用，并配备了远距离归约（distant reduction）。这使得无需借助Joachimski和Matthes原始带广义应用的ΛJ演算中所使用的广义应用的标准置换转换，就能解除β-redex的阻塞。我们证明了简单类型项的强正规化，然后通过一个定量的（即非幂等交）类型系统完整刻画了强正规化。该刻画使用了一个非平凡的强正规化归纳定义——与文献中其他定义相关——该定义基于弱头正规化策略。我们还证明了我们的演算λJn通过一种忠实的翻译与显式替换演算相关联，其意义在于该翻译保持强正规化。此外，我们的演算λJn与原始ΛJ演算确定了等价的强正规化概念。因此，λJ继承了到显式替换的忠实翻译，并且其强正规化也可以用为λJn设计的定量类型系统来刻画，尽管定量主体归约对置换转换不成立。
英文摘要：
We introduce a call-by-name lambda-calculus $λJn$ with generalized applications which is equipped with distant reduction. This allows to unblock $β$-redexes without resorting to the standard permutative conversions of generalized applications used in the original $Λ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 $λJn$ relates to explicit substitution calculi by means of a faithful translation, in the sense that it preserves strong normalization. Moreover, our calculus $λJn$ and the original $ΛJ$-calculus determine equivalent notions of strong normalization. As a consequence, $λJ$ inherits a faithful translation into explicit substitutions, and its strong normalization can also be characterized by the quantitative typing system designed for $λJn$, despite the fact that quantitative subject reduction fails for permutative conversions.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
