Combinatory weak reduction in lambda calculus

AbstractCombinatory logic claims to do the same work as λ-calculus but with a simpler language and a simpler reduction process. In a sense this claim is true: the classical reduction process in λ-calculus is indeed more complex than that in Combinatory logic. But by changing its definition only slightly one can define in λ-calculus a perfect analogue of combinatory reduction. This analogue was first formulated 30 years ago but it is still not as well known as it deserves, so in the present purely expository paper we shall try to make it more accessible. We shall discuss its definition, motivation and its neat relation to substitution