José Espírito Santo ; Delia Kesner ; Loïc Peyrot - A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized Applications

lmcs:10901 - Logical Methods in Computer Science, July 29, 2024, Volume 20, Issue 3 - https://doi.org/10.46298/lmcs-20(3:10)2024
A Faithful and Quantitative Notion of Distant Reduction for the Lambda-Calculus with Generalized ApplicationsArticle

Authors: José Espírito Santo ; Delia Kesner ; Loïc Peyrot

    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.


    Volume: Volume 20, Issue 3
    Published on: July 29, 2024
    Accepted on: March 1, 2024
    Submitted on: February 3, 2023
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 697 times.
    This article's PDF has been downloaded 350 times.