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

[Matthias Felleisen]

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.