Sharing in the Weak Lambda-Calculus

Despite decades of research in the λ-calculus, the syntactic properties of the weak λ-calculus did not receive great attention. However, this theory is more relevant for the implementation of programming languages than the usual theory of the strong λ-calculus. In fact, the frameworks of weak explicit substitutions, or computational monads, or λ-calculus with a let statement, or super-combinators, were developed for adhoc purposes related to programming language implementation. In this paper, we concentrate on sharing of subterms in a confluent variant of the weak λ-calculus. We introduce a labeling of this calculus that expresses a confluent theory of reductions with sharing, independent of the reduction strategy. We finally state that Wadsworth's evaluation technique with sharing of subterms corresponds to our formal setting.