Article View: comp.specification
Article #398Re: Semantic definition style
From: Peter D. Mosses
Date: Wed, 18 Nov 1992 08:33
Date: Wed, 18 Nov 1992 08:33
89 lines
5638 bytes
5638 bytes
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
Technical Details
Message-ID:
<1992Nov18.083324.27725@daimi.aau.dk>Path:
arc1-ca.pugleaf.net!sparky!uunet!charon.amdahl.com!pacbell.com!ames!haven.umd.edu!darwin.sura.net!Sirius.dfn.de!mailgzrz.TU-Berlin.DE!cs.tu-berlin.de!news.netmbx.de!Germany.EU.net!mcsun!sunic!dkuug!daimi!pdmReferences:
<720801988.16035@minster.york.ac.uk> <1992Nov11.195443.23006@cis.ohio-state.edu> <1992Nov13.084826.26088@daimi.aau.dk> <1992Nov18.010421.11712@cis.ohio-state.edu>Show Full Headers
Complete Article Headers
Newsgroups: comp.specification Path: arc1-ca.pugleaf.net!sparky!uunet!charon.amdahl.com!pacbell.com!ames!haven.umd.edu!darwin.sura.net!Sirius.dfn.de!mailgzrz.TU-Berlin.DE!cs.tu-berlin.de!news.netmbx.de!Germany.EU.net!mcsun!sunic!dkuug!daimi!pdm From: pdm@daimi.aau.dk (Peter D. Mosses) Subject: Re: Semantic definition style In-Reply-To: ogden@seal.cis.ohio-state.edu (William F Ogden) Message-ID: <1992Nov18.083324.27725@daimi.aau.dk> Summary: over and out Keywords: structural operational semantics, denotational semantics, nondeterminism Sender: pdm@daimi.aau.dk (Peter D. Mosses) Reply-To: pdm@daimi.aau.dk (Peter D. Mosses) Organization: DAIMI: Computer Science Department, Aarhus University, Denmark References: <720801988.16035@minster.york.ac.uk> <1992Nov11.195443.23006@cis.ohio-state.edu> <1992Nov13.084826.26088@daimi.aau.dk> <1992Nov18.010421.11712@cis.ohio-state.edu> Date: Wed, 18 Nov 92 08:33:24 GMT Lines: 89