Weak optimality, and the meaning of sharing

Abstract

In this paper we investigate laziness and optimal evaluation strategies for functional programming languages. We consider the weak lambda-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 lambda-calculus. We prove that the usual implementation of call-by-need using sharing is optimal, that is, normalizing any lambda-term with call-by-need requires exactly the same number of reduction steps as the shortest reduction sequence in the weak lambda-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.