A Faithful and Quantitative Notion of Distant Reduction for Generalized Applications
José Espírito Santo, Delia Kesner, Loïc Peyrot · Lecture notes in computer science · 2022
Abstract We introduce a call-by-name lambda-calculus $$\lambda J$$ λJ with generalized applications which integrates a notion of distant reduction that allows to unblock $$\beta $$ β -redexes without resorting to the permutative conversions of generalized applications. We show strong normalization of simply typed terms, and we then fully characterize strong normalization by means of a quantitative typing system. This characterization uses a non-trivial inductive definition of strong normalization –that we relate to others in the literature–, which is based on a weak-head normalizing strategy. Our calculus relates to explicit substitution calculi by means of a translation between the two formalisms which is faithful, in the sense that it preserves strong normalization. We show that our calculus $$\lambda J$$ λJ and the well-know calculus $$\varLambda J$$ ΛJ determine equivalent notions of strong normalization. As a consequence, $$\varLambda J$$ ΛJ inherits a faithful translation into explicit substitutions, and its strong normalization can be characterized by the quantitative typing system designed for $$\lambda J$$ λJ , despite the fact that quantitative subject reduction fails for permutative conversions.