From: pdm@daimi.aau.dk (Peter D. Mosses)
Subject: Re: Semantic definition style
Summary: over and out
Keywords: structural operational semantics, denotational semantics, nondeterminism
Reply-To: pdm@daimi.aau.dk (Peter D. Mosses)
Organization: DAIMI: Computer Science Department, Aarhus University, Denmark
Date: Wed, 18 Nov 92 08:33:24 GMT

In article <1992Nov18.010421.11712@cis.ohio-state.edu>, ogden@seal (William F Ogden) writes:
>In article <1992Nov13.084826.26088@daimi.aau.dk> pdm@daimi.aau.dk (Peter D. Mosses) writes:
>   ...
>>The style of `structural' operational semantics advocated by Plotkin
>>et al. does *not* involve any translation!  The main point is
>>precisely to avoid consideration of all the small, boring steps that
>>low-level machines make, and to specify only the bigger transitions
>>that are of interest at the programming language level.
>
>Depending upon what you're willing to accept as operational semantics, I
>suppose that the most austere forms might just reduce to denotational
>semantics. I.e., the input/output pairs from sequential denotational
>semantics (yes, pairs involving extended states which include auxillary
>components such as environments) could be viewed as just very short
>operational semantics history sequences which `specify only the bigger
>transitions that are of interest at the programming language level.'

No!  Denotational semantics is always _compositional_.  The structural
operational semantics of (e.g.) while loops is definitely not:

    <b,s> ->* <tt,s>
    --------------------------------------
    <while b do c,s> -> <c;while b do c,s>

>   ...
>Minimal fixed point operators may be no more difficult to _explain_ than
>recursive procedures, but when used with higher order functionals, they
>do seem to be more difficult for most people to _understand_.

More difficult than recursive procedures used in higher order
functional programs?  I don't agree.  One can explain minimal fixed
points operationally as gradual `unfolding'.

I think the _primary_ difficulty `most people' have with denotational
semantics is to decode intricate patterns of function composition in
lambda notation into _concepts_.  Once one sees how, say, the pattern
called continuation-passing encodes the notion of sequencing, one can
start to understand a `standard' denotational semantics.

>I never met Strachey, but from his writings at least, he doesn't strike me
>as an example of the ordinary programmers who comprise one of the three
>audiences for semantics whom we must consider.

He was indeed a programmer - but definitely not an `ordinary' one!
See Scott's foreword to Stoy's book on Denotational Semantics (MIT
Press, 1977) for some details.

>>Another, more technical drawback of the use of Scott domains in
>>denotational semantics is the following.  A semantics is usually
>>intended to specify a *class* of implementations, not just one
>>implementation.  I don't see any reason why a class of continuous
>>functions should be representable by a single continuous function.
>>E.g., consider a language where the value in an uninitialized variable
>>is an arbitrary number (not necessarily the same one each time); to
>>represent this denotationally involves unbounded nondeterminism, which
>>conflicts with the usual continuity assumption.
>
>Indeed. You don't get very far into object based programming before
>you notice that functions just don't provide an adequate base for
>the semantics of even sequential programming with objects. The
>abstraction process that permits alternative realizations of operations
>as well as information hiding inherently leads to what appears at the
>abstract object level to be nondeterminism. The obvious denotational
>semantics to cover this are relational and not functional.

You seem to have missed my point.  In the denotational semantics of
nondeterminism, one uses so-called power domains, which are quite
analogous to power sets.  Functions to power domains represent
relations!  E.g., S -> P(S) could represent a nondeterministic
state-to-state relation.  But only with _finite_branching_, if one is
to keep the usual kind of continuity.  (Apt and Plotkin investigated a
weaker form of continuity that could cope with countable
nondeterminism.)

I don't see your point about `alternative realizations'.  One gives
semantics to _programs_, each of which surely defines a _particular_
object realization?  You seem to be wanting to give semantics to loose
specifications of objects, which is a different game altogether, in my
view.

[Perhaps we should continue this by e-mail, as it probably doesn't
have sufficient general interest for comp.specification.]


-- 
Peter D. Mosses | Computer Science Department | <pdmosses@daimi.aau.dk> 
~~~~~~~~~~~~~~~ | Aarhus University           | Phone: +45 86 12 71 88 
                | Ny Munkegade, Building 540  | Fax:   +45 86 13 57 25 
                | DK-8000 Aarhus C,  Denmark  | Telex: 64767 aausci dk
Newsgroups: comp.specification