Thibaut Balabonski ; Antoine Lanco ; Guillaume Melquiond - A strong call-by-need calculus

lmcs:8650 - Logical Methods in Computer Science, March 24, 2023, Volume 19, Issue 1 - https://doi.org/10.46298/lmcs-19(1:21)2023
A strong call-by-need calculusArticle

Authors: Thibaut Balabonski ; Antoine Lanco ; Guillaume Melquiond ORCID

    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.


    Volume: Volume 19, Issue 1
    Published on: March 24, 2023
    Accepted on: January 24, 2023
    Submitted on: November 3, 2021
    Keywords: Computer Science - Logic in Computer Science

    Consultation statistics

    This page has been seen 1479 times.
    This article's PDF has been downloaded 295 times.