An operational semantics of sharing in lazy evaluation

From a theoretical point of view, lazy evaluation corresponds to the call-by-name evaluation method, which substitutes arguments for parameters before evaluating them and never evaluates under a lambda. From an implementation perspective, lazy evaluation is often equated with the call-by-need method, which is similar to call-by-name except that arguments are shared. When an argumentʹs value is required, it is evaluated and its result is stored and used for any other reference to it. The theoretical version of lazy evaluation, or call-by-name, is easily formalized with the reduction rules of lambda calculus. However, it has proven rather difficult to formalize the rules of lazy evaluation with sharing, or call-by-need, in such a way that it both captures sharing and is useful for reasoning.