[r6rs-discuss] Re: operational or denotational semantics?

From: Matthias Felleisen <matthias>
Date: Sun Feb 25 23:08:08 2007

On Feb 25, 2007, at 9:19 PM, Thomas Lord wrote:

> Matthias Felleisen wrote:
>>
>> Since Scheme is still observably sequential, I urge you to use the
>> category of Observably Sequential Functions instead of plain
>> Continuous Functions just so that the denotational equivalence
>> gets closer to truth (observational equivalence, as defined via
>> denotations).
>
> I'll look into that since I am not familiar with Observably
> Sequential Functions. I do like your use of the word "still,"
> there :-)

[I doubt others on this list are much interested so this is my last
public response on op vs den semantics, but I'll respond privately.]

Based on other messages, I take it that you know Scott/Milner/Plotkin
on Full Abstraction/FA (69-76).

  -- there is quite some intermediate work on stable functions and
related models
     [not directly relevant: Berry, Levy, Curien, Donahue,
Cartwright, Demers]
  -- Cartwright & Felleisen POPL 92
  -- Cartwrightm Kanneganti and Felleisen REX [LNCS 666, not a joke]
  -- Kanneganti and Cartwright [ICALP 93]
  -- Cartwright, Curien, and Felleisen [InfoCon 95]

 From there follow Abramsky and his school of students on Game Theory
for PCF and extensions of PCF (e.g., Thielecke). I will freely admit
that I don't know whether we have the mathematical tools yet to
construct a really good denotational semantics for R6R Scheme (yet)
but if they exist, they will be in there.

I will also freely admit that constructing and FA semantics for
Scheme isn't necessary per se but people who push denotational
semantics should be aware that so far no theorems about entire
effectful languages have been more easily proven in Den Sem models
than in Op Sem. The true reason to ask for a denotational semantics
is because you want more mathematical reasoning power and the best
one you can get is a den sem that satisfies FA.

;; ---

In general:

A semantics should be useful. One use of a semantics is to prove an
internal consistency theorem, aka, a "soundness" theorem. (They are
called type soundness often but they aren't about types per se. And
yes, they apply to Scheme as much as they apply to ML.) As you may
know, proofs of such theorems using denotational semantics are
brutally complicated. Worse, the first ones for store-based languages
were faulty. (The proofs not the theorems.) This also holds for
similar theorems about the soundness of analyses etc.

My early work on operational semantics showed that we can avoid all
these complications using my form of operational semantics, which has
become known as "evaluation context semantics" -- named after the
least interesting aspect of it.

In addition, the attempts to construct a denotational semantics for
RnR Scheme have shown that (1) it is difficult to cover the whole
language (sans libraries) and (2) not insightful.

I therefore suggested at the Boston Scheme meeting to construct an
operational "evaluation" context semantics, using a tool that Robby
Findler has developed. In this framework, you can express the
semantics based on Plotkin's lambda-value calculus easily and you can
check examples.

 From what I can tell, the semantics is reasonably compact, readable,
usable via Redex (the tool he and Jacob built) and covers the entire
core language. It is difficult to argue with such an effort.
Received on Sun Feb 25 2007 - 23:08:00 UTC