Sharing in the Weak Lambda-Calculus Revisited
Abstract
In a previous paper [4] which appeared in the volume celebrating Klop’s 60th anniversary, we presented a labeled lambda-calculus to characterize the dag implementation of the weak lambda-calculus as described in Wadsworth’s dissertation [14]. In this paper, we simplify this calculus and present a simpler proof of the sharing property which allows the dag implementation. In order to avoid duplication of presentations, we mainly show here the modifications brought to the weak labeled lambda-calculus in [4]. The reader is therefore recommended to read first the companion article and later read our present paper. We are happy that this note can therefore be considered as establishing a new bridge between two friends and now senior colleagues, Jan Willem Klop and Henk Barendregt whom this work is dedicated to on the occasion of his 60th birthday.
Full text