Home » forums » LtU Forum

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

And vice versa?

I am sure it is in literature somewhere?

By marco at 2010-06-18 11:44 | LtU Forum | previous forum topic | next forum topic | other blogs | 5760 reads

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.

By neelk at Fri, 2010-06-18 12:29 | login or register to post comments

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.

By marco at Sat, 2010-06-19 10:33 | login or register to post comments

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.

By Frank Atanassow at Sat, 2010-06-19 14:26 | login or register to post comments

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

By marco at Sat, 2010-06-19 18:39 | login or register to post comments

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

By Sam Lindley at Sat, 2010-06-19 23:08 | login or register to post comments

Okidoki

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

By marco at Sun, 2010-06-20 01:49 | login or register to post comments

Plotkin's paper

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

By John Shutt at Sun, 2010-06-20 04:28 | login or register to post comments