On Thu, 15 Mar 2007, Robby Findler wrote:

The semantics does correctly model sharing (of values that aren't
procedures -- and the informal semantics does not give a complete
specification of that particular sharing anyways).

Is it possible you are misunderstanding how it works?

Here is an example of what I mean: Consider the following implementation of pairs as closures:

  (define kons (lambda (x y) (lambda (k) (k x y))))

The formal semantics then expands lists such

  (kons 1 (kons 2 (kons 3 (kons 4 (kons 5 6)))))

to expressions whose size is linear in the number of
elements, as one would expect:

  (lambda (k)
      (k
       1
       (lambda (k)
         (k
          2
          (lambda (k)
            (k
             3
             (lambda (k)
               (k 4 (lambda (k) (k 5 6))))))))))

If we add the following apparently innocuous assertion to the definition
of kons:

  (define kons (lambda (x y) (lambda (k) (some-test y) (k x y))))

my reading of the informal semantics leads me to believe that
the space behaviour will remain linear. It will indeed be linear in all practical Scheme implementations. However, the formal semantics now expands lists such as

  (kons 1 (kons 2 (kons 3 (kons 4 (kons 5 6)))))

to expressions whose size is nonlinear in the number of elements.
Instead of the previous short expression, we now get the following enormous
expression:

(lambda (k)
      (some-test
        (lambda (k)
          (some-test
            (lambda (k)
              (some-test
                (lambda (k)
                  (some-test
                    (lambda (k) (some-test 6) (k 5 6)))
                  (k 4 (lambda (k) (some-test 6) (k 5 6)))))
              (k
               3
               (lambda (k)
                 (some-test
                   (lambda (k) (some-test 6) (k 5 6)))
                 (k
                  4
                  (lambda (k) (some-test 6) (k 5 6)))))))
          (k
           2
           (lambda (k)
             (some-test
               (lambda (k)
                 (some-test
                   (lambda (k) (some-test 6) (k 5 6)))
                 (k 4 (lambda (k) (some-test 6) (k 5 6)))))
             (k
              3
              (lambda (k)
                (some-test
                  (lambda (k) (some-test 6) (k 5 6)))
                (k
                 4
                 (lambda (k) (some-test 6) (k 5 6)))))))))
      (k
       1
       (lambda (k)
         (some-test
           (lambda (k)
             (some-test
               (lambda (k)
                 (some-test
                   (lambda (k) (some-test 6) (k 5 6)))
                 (k 4 (lambda (k) (some-test 6) (k 5 6)))))
             (k
              3
              (lambda (k)
                (some-test
                  (lambda (k) (some-test 6) (k 5 6)))
                (k 4 (lambda (k) (some-test 6) (k 5 6)))))))
         (k
          2
          (lambda (k)
            (some-test
              (lambda (k)
                (some-test
                  (lambda (k) (some-test 6) (k 5 6)))
                (k 4 (lambda (k) (some-test 6) (k 5 6)))))
            (k
             3
             (lambda (k)
               (some-test
                 (lambda (k) (some-test 6) (k 5 6)))
               (k
                4
                (lambda (k)
                  (some-test 6)
                  (k 5 6))))))))))

In other words, I cannot use the formal semantics to reason about space behaviour. This is a pity, since I would like to use some version of reduction semantics to reason specifically about the space behaviour of promises (see a prior thread about the behaviour of DELAY/FORCE and the need to add a third primitive LAZY to express lazy algorithms that will run in bounded space).

Andre

_______________________________________________
r6rs-discuss mailing list
[email protected]
http://lists.r6rs.org/cgi-bin/mailman/listinfo/r6rs-discuss

Reply via email to