TY - JOUR
T1 - Foundations of strong call by need
AU - Balabonski, Thibaut
AU - Barenbaum, Pablo
AU - Bonelli, Eduardo
AU - Kesner, Delia
N1 - Publisher Copyright:
© 2017 Copyright held by the owner/author(s).
PY - 2017/9
Y1 - 2017/9
N2 - We present a call-by-need strategy for computing strong normal forms of open terms (reduction is admitted inside the body of abstractions and substitutions, and the terms may contain free variables), 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.
AB - We present a call-by-need strategy for computing strong normal forms of open terms (reduction is admitted inside the body of abstractions and substitutions, and the terms may contain free variables), 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.
KW - Call-by-need
KW - Completeness
KW - Evaluation strategies
UR - http://www.scopus.com/inward/record.url?scp=85120103593&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85120103593&partnerID=8YFLogxK
U2 - 10.1145/3110264
DO - 10.1145/3110264
M3 - Article
AN - SCOPUS:85120103593
VL - 1
JO - Proceedings of the ACM on Programming Languages
JF - Proceedings of the ACM on Programming Languages
IS - ICFP
M1 - 20
ER -