Useful Open Call-by-Need
Beniamino Accattoli, Maico Leberle
TL;DR
This paper explores the concept of useful sharing in call-by-need lambda calculus, addressing its complexities and establishing correctness and completeness in this evaluation context.
Contribution
It introduces a formal framework for useful sharing in call-by-need, proving its correctness and completeness in handling open terms.
Findings
Useful sharing is more complex in call-by-need than in call-by-name or call-by-value.
The paper provides formal proofs of correctness and completeness.
It isolates key concepts for implementing useful sharing in call-by-need.
Abstract
This paper studies useful sharing, which is a sophisticated optimization for lambda-calculi, in the context of call-by-need evaluation in presence of open terms. Useful sharing turns out to be harder in call-by-need than in call-by-name or call-by-value, because call-by-need evaluates inside environments, making it harder to specify when a substitution step is useful. We isolate the key involved concepts and prove the correctness and the completeness of useful sharing in this setting.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.