A faithful and quantitative notion of distant reduction for generalized applications

DOI10.1007/978-3-030-99253-8_15MaRDI QIDQ6181933zbMATH OpenOpenAlexFDO

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

Publication date 23 January 2024

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://arxiv.org/abs/2201.04156

zbMATH Keywords

lambda-calculusgeneralized applicationsquantitative types

Mathematics Subject Classification ID

Theory of software (68Nxx) Theory of computing (68Qxx)

Abstract: We introduce a call-by-name lambda-calculus $lambdaJn$ 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 $LambdaJ$-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 $lambdaJn$ relates to explicit substitution calculi by means of a faithful translation, in the sense that it preserves strong normalization. Moreover, our calculus $lambdaJn$ and the original $LambdaJ$-calculus determine equivalent notions of strong normalization. As a consequence, $lambdaJ$ inherits a faithful translation into explicit substitutions, and its strong normalization can also be characterized by the quantitative typing system designed for $lambdaJn$, despite the fact that quantitative subject reduction fails for permutative conversions.

Recommendations

• A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications
• scientific article; zbMATH DE number 1332643
• \(\lambda\)-calculi with explicit substitutions preserving strong normalization
• \(\lambda\)-calculi with explicit substitutions and composition which preserve \(\beta\)-strong normalization
• scientific article; zbMATH DE number 1342288

Cites work

• scientific article; zbMATH DE number 1615235 (Why is no real title available?)
• scientific article; zbMATH DE number 2061717 (Why is no real title available?)
• scientific article; zbMATH DE number 7155170 (Why is no real title available?)
• scientific article; zbMATH DE number 7650848 (Why is no real title available?)
• An abstract factorization theorem for explicit substitutions
• An equivalence between lambda- terms
• Delayed Substitutions
• Natural deduction with general elimination rules
• Structural Proof Theory as Rewriting
• The structural \(\lambda \)-calculus

Cited in

(1)

• A faithful and quantitative notion of distant reduction for the lambda-calculus with generalized applications

This page was built for publication: A faithful and quantitative notion of distant reduction for generalized applications

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6181933)