Skip to Main content Skip to Navigation
Preprints, Working Papers, ...

A strong call-by-need calculus

Abstract : 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 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.
Document type :
Preprints, Working Papers, ...
Complete list of metadata
Contributor : Guillaume Melquiond <>
Submitted on : Tuesday, February 23, 2021 - 11:47:48 AM
Last modification on : Wednesday, March 31, 2021 - 3:38:46 AM


Files produced by the author(s)


  • HAL Id : hal-03149692, version 1


Thibaut Balabonski, Antoine Lanco, Guillaume Melquiond. A strong call-by-need calculus. 2021. ⟨hal-03149692⟩



Record views


Files downloads