[r6rs-discuss] [Formal] Formal semantics should not contain complicating optimizations
On 3/15/07, AndrevanTonder <andre_at_het.brown.edu> wrote:
> On Thu, 15 Mar 2007, Robby Findler wrote:
>
> > The formal semantics makes no claim to let you reason about the space
> > behavior of your program!
>
> But the body of the document does make some solid guarantees on space,
> and further allows one to infer behaviour w.r.t. copying and sharing of
> lambda parameters. Shouldn't one of the the purposes of an operational
> (as opposed to denotational) semantics be precisely to formalize this kind of
> reasoning?
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? For example,
this is modeled correctly:
((lambda (c)
((lambda (x y)
(set-car! x 3)
(car y))
c c))
(cons 1 2))
It produces 3, as you probably expect.
You can try it out. Download the semantics and edit the
"show-examples.scm" file!
> Insofar as it does not, I would consider it incorrect.
That is not the usual meaning of the word "incorrect". Perhaps
"incomplete" or "not what I wanted". :)
But thanks for clarifying. I'm going to assume that the earlier uses
of "incorrect" were in this sense. I hope that's okay.
> I have only seriously needed an operational semantics a few times, all of which
> involved reasoning about space behaviour. An operational semantics that does
> the unnecessary copying of the current specification would have been no use to
> me in any of these cases.
Okay.
I see the value of the operational semantics in r6, as compared to the
denotational in r5 as:
- it covers a larger part of the language
- it comes with a stepper to promote experimentation
- it has simpler mathematical underpinnings
(making is accessible to a wider audience)
My dream is that every Scheme programmer can use the semantics that
comes with r6 to play around with parts of the language to see how
things work.
I don't mean to discredit the denotational semantics in r5 or
denotational semantics in general. I do, however, believe that this
operational semantics is a good fit for the Scheme report.
Robby
Received on Thu Mar 15 2007 - 14:50:57 UTC
This archive was generated by hypermail 2.3.0
: Wed Oct 23 2024 - 09:15:01 UTC