[PRL] den sem

[Matthias Felleisen]

Will, since you find my statement concerning the executability of  
denotational semantics amusing, let me post a message to the local  
mailing list here so that our students have the benefit of a  
discussion without polluting a public list.

Consider the simplistic programming language NEXEC

An expression is one of:
    F(NE)

An NE is one of:
   -- Zero
   -- Add1(NE)

Here is the Scott model for NEXEC:
    <N_bot, f>
    where
         f : N_bot -> N_bot
	f(bot) = bot
         f(i) = 1 if Turing Machine i halts if i is on the tape
         f(i) = 0 if Turing Machine i diverges if i is on the tape

The model consists of a Scott domain and a Scott continuous function  
from the domain to itself.

Here is the denotational semantics:

  FF[F(NE)]   = f(F[NE])
   F[Zero]    = 0
   F[Add1(n)] = F[n] + 1

I believe that this denotational semantics is not executable. If I am  
wrong, I'd be happy to be convinced otherwise.

;; ----

In general I believe that Scott's program really got at the following:

1. Scott domain constraints eliminate some "computational junk" but  
not all from semantic constraints.

2. To get an executable model, you need to work within a Universal  
Domain, which can embed all domains from your category of domains of  
meaning, and with a Universal Programming Language.

3. Once you have chosen a Universal Domain/Language, you prove once  
and for all that each domain and each program in the language are  
executable.

For Scott, this meant in the early papers Pomega plus LAMBDA (!=  
lambda calculus), a language of combinators that directly denote  
elements from Pomega.

Examples:

Plotkin replaced Pomega with Tomega.

Cartwright/Demers use MID, Scott's domain of Top/Bot plus a Mid  
element, without Universal Language.

Cartwright/Kanneganti used potentially infinite trees with omega- 
branching nodes and a first-order functional language.

As far as I know,

  (A) few people have done this work for other variants
  (B) few people write in Lambda these days.

People (like Mitch) who did "compiler generation/correctness from Den  
Sem" tended to stay close to (2) and (3) above but I have also  
encountered people who built their own categories without Universal  
Language and without (3) and no guarantees about executability.

-- Matthias