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

Here is a proof that this must evaluate to #t. -- Matthias


(letrec ((x (call/cc list)))
   (if (pair? x)
       ((car x) (lambda () x))
       (pair? (x))))
=>

(letrec ((x (list *E*))
   (if (pair? x)
       ((car x) (lambda () x))
       (pair? (x)))))

where *E* =
  (letrec ((x []))
    (if (pair? x)
        ((car x) (lambda () x))
        (pair? (x))))

=>

(if (pair? (list *E*))
     ((car (list *E*)) (lambda () (list *E*)))
     (pair? ((list *E*))))

=>

((car (list *E*)) (lambda () (list *E*)))

=>

(*E* (lambda () (list *E*)))

=>

(letrec ((x (lambda () (list *E*))))
    (if (pair? x)
        ((car x) (lambda () x))
        (pair? (x))))

=>

(if (pair? (lambda () (list *E*)))
     ((car (lambda () (list *E*))) (lambda () (lambda () (list *E*))))
     (pair? ((lambda () (list *E*)))))

=>

(pair? ((lambda () (list *E*))))

=>

(pair? (list *E*))

=>

#t