Foundations of Strong Call by Need

THIBAUT BALABONSKI; PABLO BARENBAUM; EDUARDO BONELLI; DELIA KESNER

Proceedings of the ACM on Programming Languages

ASSOC COMPUTING MACHINERY

Lugar: New York, NY; Año: 2017 vol. 1 p. 1 - 29

We present a call-by-need strategy for computing strong normal forms (reduction is admitted inside the body of abstractions and substitutions), which guarantees that arguments are only evaluated when needed and at most once. The strategy is shown to be complete with respect to β-reduction to strong normal form. The proof of completeness relies on two key tools: (1) the definition of a strong call-by-need calculus where reduction may be performed inside any context, and (2) the use of non-idempotent intersection types. More precisely, terms admitting a β-normal form in pure lambda calculus are typable, typability implies (weak) normalisation in the strong call-by-need calculus, and weak normalisation in the strong call-by-need calculus implies normalisation in the strong call-by-need strategy. Our (strong) call-by-need strategy is also shown to be conservative over the standard (weak) call-by-need. Potential applications of this work are the efficient implementation of proof checkers based on dependent types and partial evaluation.