[PRL] den sem

[Matthias Felleisen]

On Feb 28, 2007, at 3:33 PM, Mitchell Wand wrote:

> Umm, if I recall the correspondence correctly, I believe that what  
> Will claimed was that a denotational semantics could either be  
> executable or not executable.  So your example merely confirms that  
> position.

Perhaps I am really old, but you reversed the positions. I (wanted  
to) say that denotational specs don't have to be executable and Will  
made fun of my statement.

> <requires="math">

Yes, I am aware of this. I used to teach Den Sem at Rice starting  
from Plotkin's PCF paper and especially the enumerability and the  
Exists function. (It's an example of an infinite function that isn't  
expressible in the syntax of PCF but exists in the domain. Hence he  
needed to add it to the syntax of PCF. In SPCF/ObsSeqFuncts,  this  
particular problem completely goes away. CATCH is enough.)

(You're probably right about my specific function, but that doesn't  
matter. I can construct another f that illustrate the same thing.)

> As to What Mitch Did:
>
> You can do this for any intermediate language that has an adequate  
> opsem/densem pair.  Universal Domains or Calculi are not needed,  
> though of course they provide a handy source of such intermediate  
> languages.

That is correct of course. You don't need Universal Domains/Languages  
but those make it more efficient to work out executable denotational  
specs.

-- Matthias