[r6rs-discuss] [Formal] Delayed evaluation

[Andre van Tonder]

On Mon, 18 Sep 2006, AndrevanTonder wrote:

  >    We may verify that the above *incorrect* encoding of the example,
  >    using (delay (force ---)), does *not* run in bounded space
  >    (since the size of the expression below grows without bound):
  >  ...

  I somehow cut the first step in this example.  Here it is in full:

       (let (loop) (delay (force (loop))))

       (force (loop)) --> (force (delay (force (loop))))
                       =  (let ((p (delay (force (loop)))))    (beta-equiv)
                            (force p))
                      --> (let ((v (force (loop))))  ---- (*)
                            (let ((p (delay v)))
                              v)
                      --> (let ((v (force (delay (force (loop))))))
                            (let ((p (delay v)))
                              v)
                       =  (let ((p (delay (force (loop)))))
                            (let ((v (force p)))
                              (let ((p (delay v)))
                                v)
                       =  (let ((v (force (loop)))) ---- one more level than (*)
                            (let ((p (delay v)))
                              (let ((v (force p)))
                                (let ((p (delay v)))
                                  v)
                      --> etc.
         ==> UNBOUNDED SPACE CONSUMPTION

Andre