A faithful and quantitative notion of distant reduction for generalized applications

DOI10.1007/978-3-030-99253-8_15arXiv2201.04156OpenAlexW4225832821MaRDI QIDQ6181933FDOQ6181933

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)

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.

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

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

zbMATH Keywords

lambda-calculusgeneralized applicationsquantitative types

Mathematics Subject Classification ID

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

Cites Work

• Natural deduction with general elimination rules
• An equivalence between lambda- terms
• Delayed Substitutions
• The structural \(\lambda \)-calculus
• Structural Proof Theory as Rewriting
• Title not available (Why is that?)
• An abstract factorization theorem for explicit substitutions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Title not available (Why is that?)

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)