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

Fair enough. I should have known better.
I used callcc to extract set! out of letrec's back in 1987.

-- Matthias



On Aug 19, 2008, at 10:10 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.
>
> I believe that matches the semantics of PLT Scheme's `letrec'.
>
> The R5RS/R6RS `letrec' is different, and the result with that other
> `letrec' should be #f:
>
>
> (letrec ((x (call/cc list)))
>    (if (pair? x)
>        ((car x) (lambda () x))
>        (pair? (x))))
>
> =
>
> (let ((x #f))
>    (set! x (call/cc list))
>    (if (pair? x)
>        ((car x) (lambda () x))
>        (pair? (x))))
>
> =>
>
> (define x_0 #f)
> (begin
>   (set! x (call/cc list))
>   (if (pair? x_0)
>       ((car x_0) (lambda () x_0))
>       (pair? (x_0)))))
>
> =>
>
> (define x_0 #f)
> (begin
>   (set! x (list *E*))
>   (if (pair? x_0)
>       ((car x_0) (lambda () x_0))
>       (pair? (x_0)))))
>
> where *E* =
>   (begin
>     (set! x_0 [])
>     (if (pair? x_0)
>         ((car x_0) (lambda () x_0))
>         (pair? (x_0))))
>
> =>
>
> (define x_0 (list *E*))
>
> (if (pair? x_0)
>     ((car x_0) (lambda () x_0))
>     (pair? (x_0)))
>
> =>
>
> (define x_0 (list *E*))
>
> (if (pair? (list *E*))
>     ((car x_0) (lambda () x_0))
>     (pair? (x_0)))
>
> =>
>
> (define x_0 (list *E*))
>
> ((car x_0) (lambda () x_0))
>
> =>
>
> (define x_0 (list *E*))
>
> (*E* (lambda () x_0))
>
> =>
>
> (define x_0 (list *E*))
>
> (begin
>  (set! x_0 (lambda () x_0))
>  (if (pair? x_0)
>      ((car x_0) (lambda () x_0))
>      (pair? (x_0))))
>
> =>
>
> (define x_0 (lambda () x_0))
>
> (if (pair? x_0)
>     ((car x_0) (lambda () x_0))
>     (pair? (x_0)))
>
> =>
>
> (pair? (x_0))
>
> =>
>
> (pair? ((lambda () x_0)))
>
> =>
>
> (pair? x_0)
>
> =>
>
> (pair? (lambda () x_0))
>
> =>
>
> #f
>