论文标题
lambda-calculus的遥远降低概念，并具有广义应用
A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications
论文作者
论文摘要
我们介绍了带有通用应用程序的通用lambda-calculus $λjn$，该应用程序配备了远处的减少。这允许解除$β$ -REDEXES，而无需诉诸于原始$λj$ -calculus中使用的广义应用程序的标准置换转换，并具有Joachimski和Matthes的广义应用。我们显示了简单型术语的强范围，然后我们通过定量（即非数字相交）键入系统充分表征强归一化。该表征使用强归一化的非平凡归纳定义 - 与文献中的其他人相关 - 基于弱头归一化策略。我们还表明，我们的微积分$λjn$通过忠实的翻译与明确的替代划线有关，从某种意义上说，它可以保持强大的归一化。此外，我们的微积分$λjn$和原始的$λj$ -calculus确定了强范围的等效概念。结果，$λ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.
