Okay, sure. You've said that several times now. I agree (for the
second time): the semantics cannot be used to reason about space
behavior!
You also stated that the semantics gets sharing wrong. If all you mean
is the below, then I understand what you mean there is nothing more to
say, as far as I'm concerned.
But, just in an attempt to be clear to you, I'm claiming that there is
no observable way in which sharing is wrong. In yet more words, there
is no program that produces 3 when it should produce 4, due to missed
sharing (not that the 3 and 4 are important, except that they are
different from each other).
Robby
On 3/16/07, AndrevanTonder <andre_at_het.brown.edu> wrote:
> 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 - 12:33:41 UTC