[r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations

From: AndrevanTonder <andre>
Date: Fri Mar 16 11:35:27 2007

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
Received on Fri Mar 16 2007 - 11:34:48 UTC