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.

### Like this:

Like Loading...

*Related*

What’s the meaning of “[x'/x]” in the term t>u[x'/x] in application evaluation?

is the term with variable substituted by term .