[PRL] den sem, some additional comments

[William D Clinger]

For the benefit of our graduate students, continued...

Matthias wrote:

> 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.

I said "Thanks to greater awareness of Church's thesis
and computability in general...".  In other words, the
referees aren't quite so naive about computability now
as they were a few decades ago.

> I think your argument is unacceptable. It basically argues that every  
> "program" written in a "programming language" (TM, LC, Scheme) is a  
> denotational semantics.

I argued nothing of the sort.  What I wrote is that any
denotational semantics that is expressed by an executable
program is executable.  I also provided a link to source
code for a specific program that expresses an operational
semantics for Turing machines that is not denotational,
which serves as a concrete counterexample to your
accusation.

> ....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).

I agree that you need to be careful.  As a constructive
mathematician, I am careful about that kind of thing by
force of long habit; I need not hesitate to use the most
appropriate domains and metalanguages for the problem at
hand.  Most of the people who do research in denotational
semantics are at least as competent as I am.

> 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.

I identified two specific areas in which operational
semantics tends to be more useful than denotational:
proving the correctness of compiler optimizations, and
describing the semantics of nondeterministic languages.
I never implied that was an exhaustive list.

> 3. I share and don't share your evaluation of full abstraction as a  
> minor impediment....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.

I explained why full abstraction is basically irrelevant
to proving the correctness of most compiler optimizations:
those optimizations are mostly about recognizing and then
exploiting the special cases that are by far the most
common in actual programs, whereas full abstraction has to
do with interchangeability in all contexts, no matter how
theoretical and bizarre.

> 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).

That anecdote supports my position, and undermines yours.

BTW, Presburger's name contains only one 's'.

Will