A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications
José Espírito Santo, Delia Kesner, Loïc Peyrot
TL;DR
This work studies a call-by-name lambda calculus with generalized applications, introducing distant β to unblock β-reductions without relying on the π permutation. It provides a complete quantitative account of strong normalization via a non-idempotent intersection-type system and an inductive ISN (strong normalization) characterization, along with a faithful translation to explicit substitutions. A faithful ES translation is shown to preserve and reflect strong normalization, and the authors establish equivalence of strong normalization across the λJn, ΛJ, and β,π/β+p2 frameworks. They also demonstrate that π is not quantitative, motivate the distance-based approach, and connect the findings to explicit substitutions, yielding a robust, faithful bridge between these formalisms with concrete implications for type-based normalization bounds and reasoning about sharing via generalized applications.
Abstract
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.