Optimal reduction in the lambda calculus

Lambda the Ultimate links to a new paper, Lambdascope, that describes an implementation of optimal reduction in the lambda calculus.

Optimal, in this case, means the minimum amount of duplication. Usually, when you apply a function in the lambda calculus, you must make a copy of the function body before you start evaluating. In his 1978 thesis, Levy showed that some of this copying could be redundant; in some cases, exponentially so. Levy did not provide an algorithm for optimal reduction, but several have since been invented.

Optimal reduction is a refinement of lazy evaluation. In lazy evaluation, arguments to functions are only copied as needed. Laziness minimizes copying on the right side of function applications, while optimal reduction minimizes it on both sides.

Implementations of optimal reduction are incredibly difficult to understand. The one in the lambdascope paper looks simpler, but I haven’t fully assimilated it.