2026-07-24T10:25:23Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:14247 2024-03-06T10:53:15Z ddc:004 open_access

A Strong Call-By-Need Calculus Balabonski, Thibaut Lanco, Antoine Melquiond, Guillaume strong reduction call-by-need evaluation strategy normalization We present a call-by-need λ-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 λ-term t admits a normal form n in the λ-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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Thibaut Balabonski and Antoine Lanco and Guillaume Melquiond 2021 Is Part Of LIPIcs, Volume 195, 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2021.9 urn:nbn:de:0030-drops-142477 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2021.9 eng https://creativecommons.org/licenses/by/4.0/legalcode