[Prev][Next][Index][Thread]

"foundations built on sand"

I am glad to see that I have (unintentionally) triggered a discussion about 
the usefulness of semantic methods. I think that is an important point. For me
it is evident from the following few examples less of engineering style than
the ones provided up to now

1) ML was developed triggered by "foundational" work on PCF
   (at least that's how it appears to me from my fairly incomplete
    record of history)

2) purely mathematically motivated work on "Normalization by Evaluation" (NbE)
   was found interesting by the partial evaluation community (O.Danvy could
   say much more about it); for sake of completeness I should add that NbE
   was invented by Schwichtenberg and Berger for very practical purposes,
   namely using the Scheme interpreter for performing normalisation;
   such an interaction of theory and practice seems to be the ideal case and
   it's rather the exception than the rule, I am afraid

3) type theoretic work using semantical methode was done my M.Hofmann to
   manufacture type systems guaranteeing certain complexity behaviours;
   similar results were obtained by syntactical methods by Schwichtenberg,
   Bellantoni and Niggl.

This last example also brings to the point that one NEED not insist on 
denotational methods, also operational or proof-theoretic methods definitely
can do the job. Just sometimes denotational methods are more concise and, 
therefore, much easier to grasp.

This brings me back to my original question concerning translation of SOOL
to META + F_{sub,rec,state}. From my point of view everything would be ok 
if the target language  F_{sub,rec,state}  were endowed with an appropriate 
operational semantics. I haven't seen such work and it is not contained in the
FOOL book. Some of it is sketched there but operational semantics of state 
isn't dealt with at all and that's what I consider most critical.
As I understand the main theorem is that

   (Sound) if  t : A  in SOOL then  [|t|] : [|A|]  in META

this definitely should be accompanied by a proof that

   (Refl)  if [|t|] doesn't give rise to a run time error 
           then t doesn't give rise to a run time error
 
This second property is rather assumed than proved. That's my impression 
though I really might be mistaken as I didn't read everything in detail.

In any case I don't insist on denotational models though I definitely prefer
them when available. Also operational methods may allow one to find 
conceptually clear invariants (`a la logical relations) that allow one to 
guarantee the absence of some undesired effects.

Thomas