[PRL] den sem

[Mitchell Wand]

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.

<requires="math">
If you want to really add computability to the story, then you have to start
by enumerating a countable basis {e_1, ...} for your domain and insisting
that all your functions are "representable" in a sense much like the
following:

A function f : D -> D is representable iff there exists a recursive relation
R(i,j) on the integers such that e_j \le f(e_i) iff (i,j) \in R.

I doubt that the function f in your example is computable in this sense.
</requires="math">

As to What Mitch Did:

What Mitch did was to observe that most common denotational semantics are in
fact compositional translations from the source language to some lambda
calculus.  These translations are also computable, which is entirely
orthogonal.

Wadsworth's theorem & its cousins establish that certain reduction
strategies are adequate for certain models of certain lambda calculi.  For
Wadsworth, this was the untyped lambda-calculs and D_\inf.  Furthermore,
these reduction strategies were computable.

So to make your "denotational semantics" "executable", you take your source
program, translate it to a lambda-term (this step is computable), and then
apply the reduction strategy to the translated term (this step is also
computable).  Voila!

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.

--Mitch



On 2/28/07, Matthias Felleisen <matthias at ccs.neu.edu> wrote:
>
>
> 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
>
>
>
>
> _______________________________________________
> PRL mailing list
> PRL at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/prl
>
>
-------------- next part --------------
HTML attachment scrubbed and removed