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.


Post to Twitter

Escribe un comentario