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

From: Robby Findler <robby>
Date: Thu Mar 15 14:51:31 2007

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