Happy new year! Today was the first theory lunch of 2013 and I talked about lazy, or call-by-need evaluation.
Call-by-need strategy evaluates a (function) argument only when needed and the evaluation is shared among all the uses of the argument.
We looked at natural semantics for call-by-need.
The syntax of the language — a tiny lambda calculus.
A heap, ranged over by , maps variables to expressions.
A configuration is a pair of a heap and an expression.
A configuration is closed if and for all , — we only consider closed configurations.
Evaluation judgment states that evaluating the expression in the heap returns a value with the heap being .
Let’s look at evaluation relations.
Evaluating a value returns immediately:
To evaluate a variable, we consult the heap. We have two cases.
If the variable is already bound to a value in the heap, then we are done:
If the expression bound to the variable is not yet evaluated, then the expression has to be evaluated.
Note that the resultant heap is updated to map to , memorizing the evaluation.
Finally evaluation of application:
We first evaluate the function expression to a lambda abstraction, then allocate the argument in the heap with a fresh varialbe and continue to evaluate the body of the lambda expression.