[PRL] den sem, some additional comments

[Matthias Felleisen]

Will, so I agree with your write-up but after some reflection I do  
have comments:

1. You say that due to Church's thesis, it is no longer necessary to  
waste pages on proving that the meta-language is executable. (If my  
recollections are wrong, I know you want hesitate calling me things.)  
I think your argument is unacceptable. It basically argues that every  
"program" written in a "programming language" (TM, LC, Scheme) is a  
denotational semantics. To me, this is not the point of denotational  
semantics, as a form of specification from logic.

I used LAMBDA as in Scott's papers, which is NOT the lambda calculus.  
Instead it is a collection of mathematical functions that can easily  
be mapped to Pomega elements and that are executable. The  
combinations of these things are executable, too. If you use  
mathematical functions on, say, Scott domains outside of that  
collection, you are not assured executability. So I do think that you  
need to nail down mathematical structures and functions on top of  
them to write specs and you need a filter to ensure executability  
(e.g., Scott domains + LAMBDA, CCC plus typed lambda w/ fix, OSF  
domains + "Kleene", etc).

2. You also express the opinion that subjective factors plus non- 
determinism have contributed to the switch from denotational  
semantics to operational semantics. (Again, I believe that this is an  
accurate attribution.) I totally agree with the non-determinism part  
(having studied your thesis in a two-student course with you and  
having heard de Bakker and de Roever speak on metrics and Banach  
spaces often enough in the late 80s and early 90s). What I don't  
completely agree with is the subjective factors part, but of course  
there is no way to validate this. I do think it is interesting to  
know the story however:

[1970s]  the complexity of relating one den sem to another (Reynolds  
"logical predicates in the untyped world")
[1980s]  the failure of Damas thesis to prove type soundness for  
imperative ML using denotational semantics
[70/80s] the simultaneous discovery that den sem just doesn't hack it  
for non-deterministic systems
[70/80s] the "translation" of den sem into SOS by Plotkin
[88/89]  the complexity of the proof of type soundness in Mads  
Tofte's thesis (again for imperative ML)
[90/92]  the seeming ease of a proof using reduction semantics
[80-95]  similar ease of proofs for analyses when compared to  
Cousot's work (using den sem)

In sum, the kind of theorems that people wanted to prove didn't work  
out smoothly or easily in a denotational setting but were relatively  
easy to prove in an SOS or reduction semantics setting. Usability --  
just like with software applications -- and desired "target  
usefulness" play a tremendous role.

3. I share and don't share your evaluation of full abstraction as a  
minor impediment. On one hand, I believe that the way people  
connected observational equivalence to compilation and optimization  
is naive. I worked on the problem, I consider it to this day my  
deepest result, and I am more than willing to admit it. I left the  
area behind mostly because I think it's just wonderful math and has  
little bearing on real PL design issues. On the other hand, I  
conjecture that if we could find good mathematical-logical ways to  
implement automatic reasoning about obs equiv (the ultimate goal of  
FA researchers) then compilation and optimization would benefit  
tremendously.

To this day I recall Bill Pugh's visit to Rice in the early 90s.  
Using "bird watching" of Fortran programs, plain logic, and the  
decidability of Pressburger, he had accomplished as much on standard  
Fortran benchmarks as an "army" of Ken Kennedy PhD students, post- 
docs, and research scientists. It blew them away. Just in case: he  
had observed that the language that people optimize most is "for  
loops for constants and linear calculations with addition and  
multiplication by integer constants." For this non-Turing PL, you can  
reason about equalities using Pressburger arithmetic, which is  
decidable and computable (hyper-exponentially).

I am expecting similar results from work on reasoning mathematically  
about obs equiv in general (after my death).

-- Matthias