## 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

### 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.

### Thanks

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.

### Encodings

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.]