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

Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s