Weak Optimality, and the Meaning of Sharing

Por • 19 sep, 2018 • Sección: Ciencia y tecnología

Thibaut Balabonski

Abstract In this paper we investigate laziness and optimal evaluation strategies for functional programming languages. We consider the weak λ-calculus as a basis of functional programming languages, and we adapt to this setting the concepts of optimal reductions that were defined for the full λ-calculus. We prove that the usual implementation of call-by-need using sharing is optimal, that is, normalizing any λ-term with call-by-need requires exactly the same number of reduction steps as the shortest reduction sequence in the weak λ-calculus without sharing. Furthermore, we prove that optimal reduction sequences without sharing are not computable. Hence sharing is the only computable means to reach weak optimality.

https://www.lri.fr/~blsk/Docs/Balabonski-WeakOptimality-ICFP13.pdf

Post to Twitter

Escribe un comentario