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

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