A strong call-by-need calculus

DOI10.46298/LMCS-19(1:21)2023arXiv2111.01485MaRDI QIDQ6135746FDOQ6135746

Authors: Thibaut Balabonski, Guillaume Melquiond 

Publication date: 26 August 2023

Published in: Logical Methods in Computer Science (Search for Journal in Brave)

Abstract: We present a call-by-need $lambda$-calculus that enables strong reduction (that is, reduction inside the body of abstractions) and guarantees that arguments are only evaluated if needed and at most once. This calculus uses explicit substitutions and subsumes the existing strong-call-by-need strategy, but allows for more reduction sequences, and often shorter ones, while preserving the neededness. The calculus is shown to be normalizing in a strong sense: Whenever a $lambda$-term t admits a normal form n in the $lambda$-calculus, then any reduction sequence from t in the calculus eventually reaches a representative of the normal form n. We also exhibit a restriction of this calculus that has the diamond property and that only performs reduction sequences of minimal length, which makes it systematically better than the existing strategy. We have used the Abella proof assistant to formalize part of this calculus, and discuss how this experiment affected its design. In particular, it led us to derive a new description of call-by-need reduction based on inductive rules.

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

zbMATH Keywords

normalizationcall-by-needstrong reductionevaluation strategy

Mathematics Subject Classification ID

Logic in computer science (03B70) Theory of computing (68Qxx) Computer science (68-XX)

Cites Work

• Abella: A System for Reasoning about Relational Specifications
• Call-by-name, call-by-value and the \(\lambda\)-calculus
• An extension of basic functionality theory for \(\lambda\)-calculus
• An abstract machine for strong call by value
• A strong call-by-need calculus
• The call-by-need lambda calculus
• Parametric higher-order abstract syntax for mechanized semantics
• The Call-by-Need Lambda Calculus, Revisited
• Quantitative Types for the Linear Substitution Calculus
• The locally nameless representation
• Local bigraphs and confluence: two conjectures (extended abstract)
• The structural \(\lambda \)-calculus
• A nonstandard standardization theorem
• Title not available (Why is that?)
• A compiled implementation of strong reduction
• Distilling abstract machines
• A unified approach to fully lazy sharing
• Title not available (Why is that?)
• Reasoning About Call-by-need by Means of Types
• Non-idempotent intersection types for the Lambda-Calculus
• Weak optimality, and the meaning of sharing
• A Theory of Explicit Substitutions with Safe and Full Composition
• A Strong Distillery

Cited In (4)

• An abstract machine for strong call by value
• Title not available (Why is that?)
• A mechanism of function calls in MSVL
• A strong call-by-need calculus

This page was built for publication: A strong call-by-need calculus

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