Natural semantics for call-by-need

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.

$\begin{array}{rrcl} \mathit{expressions} & t,s,u & := & x \mid \lambda x. t \mid t s \\ \mathit{values} & v & := & \lambda x.t \end{array}$

A heap, ranged over by $\Phi, \Psi$ , maps variables to expressions.

A configuration $\langle \Phi \rangle t$ is a pair of a heap and an expression.

A configuration $\langle \Phi \rangle t$ is closed if $\textit{FV}(t) \subseteq \textit{dom}(\Phi)$ and for all $x \in \mathit{dom}(\Phi)$ , $\textit{FV}(\Phi(x)) \subseteq \textit{dom}(\Phi)$ — we only consider closed configurations.

Evaluation judgment $\langle \Phi \rangle t \Downarrow \langle \Psi \rangle v$ states that evaluating the expression $t$ in the heap $\Phi$ returns a value $v$ with the heap being $\Psi$ .

Let’s look at evaluation relations.

Evaluating a value returns immediately:

$\frac{}{\langle \Phi \rangle \lambda x. t\ \Downarrow\ \langle \Phi \rangle \lambda x. t}$

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:

$\frac{\Phi(x) = v}{\langle \Phi \rangle x\ \Downarrow\ \langle \Phi \rangle v}$

If the expression bound to the variable is not yet evaluated, then the expression has to be evaluated.

$\frac{\Phi(x) \not= v \ \langle \Phi[x\mapsto \bullet]\rangle \Phi(x)\ \Downarrow\ \langle \Psi \rangle v }{\langle \Phi \rangle x\ \Downarrow\ \langle \Psi[x \mapsto v] \rangle v}$

Note that the resultant heap $\Psi$ is updated to map $x$ to $v$ , memorizing the evaluation.

Finally evaluation of application:

$\frac{\langle \Phi \rangle s \Downarrow \langle \Phi' \rangle \lambda x.u \ \ \langle \Phi'[x'\mapsto t]\rangle u[x'/x] \Downarrow \langle \Psi \rangle v \ \ x \ \textrm{fresh}}{\langle \Phi \rangle s t \Downarrow \langle \Psi \rangle v}$

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.

2 thoughts on “Natural semantics for call-by-need”

onixie on January 9, 2013 at 8:29 am said:

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

Reply ↓
- Wolfgang Jeltsch on January 11, 2013 at 10:34 am said:
  
  $u[x'/x]$ is the term $u$ with variable $x$ substituted by term $x'$ .
  
  Reply ↓