Looking for a proof that eager reduction is as strong as lazy reduction

And vice versa?

I am sure it is in literature somewhere?

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

I don't know what you mean by "strong"...

...but you can encode cbn in cbv languages, and vice-versa using a CPS translation. IIRC Gordon Plotkin proved this in 1975, "Call-by-Name, Call-by-Value, and the Lambda Calculus". It's an old enough result that someone must have figured out an incredibly slick presentation by now.


I mean they are both Turing complete. I was looking for something more direct though, my initial thoughts were in the direction of a lambda self evaluator, which takes an (encoded) term, and when eagerly reduced, gives back the normalized term.

CBV diverges strictly more often.

Eager reduction is "weaker" in the sense that:

  • if a term has a normal form under lazy reduction, eager reduction will sometimes diverge, but
  • if a term has a normal form under eager reduction, lazy reduction will always find it.

Put differently, the CBV terms that converge are a strict subset of CBNeed terms that converge.

Whether you consider this evidence of "weakness" is up to you.


Just to make it clear. I am looking for Turing equivalence. An informal proof that eager reduction is equivalent in strength to lazy reduction: Haskell runs on i386, Haskell can emulate i386.

So, what I am looking for is the shortest formal proof of that notion.

[Not sure, I guess we agree.]

As neelk already said,

As neelk already said, Gordon Plotkin's seminal paper from 1975 should give you what you want. It may be a tad dated, but it is quite accessible... assuming you can find a copy.

If you want something a bit more modern (and easier to download from the Internet), then you might want to look at the work of Hatcliff and Danvy. First, they generalised Plotkin's work in "A generic account of continuation-passing styles". Then they did the same thing using thunking translations in place of CPS translations in "Thunks and the lambda-calculus".


So I am reading through the reference, I just hoped something simpler would come up. Anyway, thanks to both then.

Plotkin's paper

For the record, Plotkin's paper is available here.