How am I misunderstanding call-by-need evaluation?

Question

First of all, I never studied these things or anything, so I may be asking very silly questions, which I am sorry for, but please go easy on me :)

I'm playing around with implementing lambda calculus, with call-by-need evaluation. I'm trying to follow this paper on the subject, where the relevant bit seems to be the natural semantics described on page 28.

Anyway, what I don't understand about this evaluation strategy is that, as far as I understand, the actual substitution only happens when evaluating variables. Abstractions evaluate to themselves, as these are the values, and applications only add new entries to the cache.

But given that, how exactly one go about evaluating a term like

(λx.λy.x y) λa.a

According to the natural semantics, described in the linked paper, the first evaluation step would be to add the entry x -> λa.a to the cache, and evaluate the body of the abstraction on the lhs of the application, which is λy.x y. But this is a value, so the evaluation ends. At which point we have a term that is not closed, and a non-empty heap. While we know exactly that this term should evaluate to λy.(λa.a) y.

What am I misunderstanding? How does this work in languages that actually use this evaluation strategy?

Answer 1

Your reduction is right. The point is that the call by need strategy addressed in that paper is only a weak strategy, in the sense that it will never reduce under a lambda expression. This is evident in Fig.1, where the expression \x.M is a value.

At the end of the reduction, if you want to obtain a lambda term explicitly, you still need to unwind the cache (frequently called environment in the literature), that amounts to substitute the associations in the cache inside your term:

                λy.x y [x -> λa.a] = λy.(λa.a) y

as expected.