[plt-scheme] about letrec and continuation : which behavior is correct ? and why ?

On Aug 19, 2008, at 10:22 AM, Matthew Flatt wrote:

> At Tue, 19 Aug 2008 09:59:44 -0400, Matthias Felleisen wrote:
>> Here is a proof that this must evaluate to #t.
>
> Actually, on further investigation, I don't think that PLT Scheme's
> `letrec' is supposed to behave that way, either. Your proof is  
> treating
> `letrec' like `let', right?

Correct. That was my mistake if you take the RnRS set! definition
as the semantics of letrec. If, however, you agree that letrec is
to find the fixed point of the equation x = (call/cc list), I think
a let-style semantics is appropriate because x doesn't occur on the
right side of the equation.

[NB. I do believe that Bob Hieb showed me how this worked in Chez
way back, i.e., it also computes the FV set of the right-hand sides
and replaces a letrec with a nest of let/let* computations. Of
course Kent may have changed that since then.]

> That's exactly what MzScheme's optimizer is
> incorrectly doing in this case.

Depends on what we define letrec to mean.

> So I'm now pretty sure that the right answer is #f for all of our
> variations on `letrec', and I'll fix the optimizer.

Yes I can see an argument for having a set! style semantics in all
cases.

-- Matthias