NetNews Usenet Archive 1992 #27/NN_1992_27.iso/spool/comp/specific/548

Text File | 1992-11-22 | 9.8 KB | 235 lines

Newsgroups: comp.specification
Path: sparky!uunet!mcsun!sunic!dkuug!daimi!pdm
From: [e-mail] (Peter D. Mosses)
Subject: Re: Semantic definition style
In-Reply-To: [e-mail] (Peter D. Mosses)
Message-ID: <[e-mail]>
Summary: Re-post of references for action semantics
Keywords: structural operational semantics, denotational semantics,
    nondeterminism, action semantics, bibliography, FTP
Sender: [e-mail] (Peter D. Mosses)
Reply-To: [e-mail] (Peter D. Mosses)
Organization: DAIMI: Computer Science Department, Aarhus University, Denmark
References: <[e-mail]> <[e-mail]> <[e-mail]> <[e-mail]> <[e-mail]> <piotr.722190155@sedalia> <[e-mail]>
Date: Mon, 23 Nov 92 06:09:17 GMT
Lines: 218

In article <[e-mail]>, I wrote:
> ... namely action semantics (references provided in an earlier
>message - mail me if you missed that one).

Apparently quite a few of you missed the earlier message (and I never
saw any responses to it).  Here it is again, together with another
earlier message that indicated how to FTP the action semantics
bibliography:

Newsgroups: comp.specification
From: [e-mail] (Peter D. Mosses)
Subject: Re: Semantic definition style
Summary: Action semantics is best :-)
Keywords: action semantics, action notation, denotational semantics,
    operational semantics

In article <[e-mail]>, bevan@cs (Stephen J Bevan) writes:
>In article <[e-mail]> [e-mail] (Dave Mason) writes:
>   In article <[e-mail]> [e-mail] writes:
>   > I am aware that there are four different styles to define semantics.
>   >     operational
>   >     denotational
>   >     algebraic
>   >     axiomatic
>
>   There is also action semantics, as describes by Mosses.  In many ways,
>   action semantics is better than the others, but it's also newer.
>
>I don't want to start a "my spec. system better than your spec.
>system" but would you (or anybody else) care to expand on the above?
>
>My only exposure to action semantics is via a couple of tech reports
>and David Watt's book [1].  From this I get the impression that great
>emphasis is put on the readability aspect of the definition.  However,
>I'm at a loss to see the difference between the action semantic
>definitions given and an equivalent denotational/operational
>definition that uses equally well chosen English words instead of
>Greek symbols[2].  There must be more to it than just notation, so
>could somebody please enlighten me?
>
>bevan

Sorry, I was away and missed Dave Mason's message.  So let me react
just to the above, which is a crucial point.  I'll try to be brief.

First of all, please note that a complete reference manual and text
book for action semantics (AS) has recently been published [3].  Not
only does the book provide the formal foundations of the AS framework,
but also it demonstrates the modularity of AS descriptions: when one
adds new language features, one *never* has to make the kind of
large-scale reformulation of previous semantic equations that is known
from denotational semantics (DS).

Now to the point raised above.  In fact one *can* use action notation
(AN) as an auxiliary notation in DS, defining the action primitives
and combinators as higher-order functions on domains.  See [4] for an
example.  Then the semantic equations look just the same as with AS!
When adding new language features, one now avoids changes to the
semantic equations themselves; but it may be necessary to change the
definitions of the auxiliary notation, of course.  AS avoids the need
for changes altogether by having a fixed (operational) semantics for
the entire AN.

A more technical problem with using AN in DS is to get a model (of the
full AN) that satisfies all the desired laws: actions involve
unbounded nondeterminism and interleaving, and it seems impossible to
get fully abstract models for them, even though their operational
semantics is quite straightforward.

Regarding operational semantics (OS): the usual structural approach
involves the syntax of the described language as components of
configurations.  Repetitious inference rules determine, say,
left-to-right expression evaluation in various constructs.  With AS,
one uses a single combinator of AN (`A1 and then A2') to express the
concept of sequential evaluation; the inference rules for *its* OS
have been given, once-and-for-all.  The AS semantic equations can be
regarded as a compiler into AN, so the OS of AN (given in [3]) does
indeed allow an AS decsription to be seen as an OS - but not as one
that is structural in the usual sense.

Finally, let me point out that David Watt and I spent many years on
the design of our standard AN.  The starting point was a direct
representation of the fundamental concepts of programming languages as
developed by Christopher Strachey (in DS, these concepts get `coded'
as particular patterns of function composition).  We also took account
of desirable algebraic laws, e.g., all the binary combinators of AN
are associative, and have units.  However, our experimentation with AS
descriptions of realistic programming languages has substantially
influenced AN.  By having a *standard* AN, we facilitate large-scale
reuse of semantic descriptions.  The use of English words rather than
Greek (and mathematical) symbols increases readability - also
writability! - but is not essential for obtaining the other pragmatic
advantages of the AS framework.

>[1]
>@book
>{ Watt91
>, author=    {David A. Watt}
>, title=     {Programming Language Syntax and Semantics}
>, publisher= {Prentice Hall International}
>, year=      {1991}
>}
>
>[2] Use monads if you want to hide "state" and/or "enviroments" in a
>    similar fashion to the facets in an action semantic definition :-

... but it isn't so easy to combine various monads without
reformulating semantic equations!  Are there any larger semantic
descriptions based on monads?

>@inproceedings
>{ Moggi89
>, author=    {E. Moggi}
>, title=     {Computational lambda-calculus and monads}
>, booktitle= {IEEE International Symposium on Logic In Computer Science}
>, year=      {1989}
>}
>
>@techreport
>{ Wadler92
>, author=      {Philip Wadler}
>, title=       {Comprehending Monads}
>, institution= {Department of Computing Science, University of Glasgow}
>, address=     {Glasgow, UK, G12 8QQ}
>, year=        {1992}
>}

[3]
@book{Mosses92as,
    title = {Action Semantics},
    publisher = "Cambridge University Press",
    year = {1992},
    author = {Peter D. Mosses},
    series = {Cambridge Tracts in Theoretical Computer Science},
    number = {26}
}

[4]
@incollection{Mosses91pids,
    author = {Peter D. Mosses},
    title = {A Practical Introduction to Denotational Semantics},
    booktitle = {Formal Description of Programming Concepts},
    year = {1991},
    publisher = "Springer-Verlag",
    editor = {Ehrich J. Neuhold and Manfred Paul},
    pages = {1--49},
    series = {{IFIP} State-of-the-Art Reports}
}


From: [e-mail] (Peter D. Mosses)
Subject: Re: Semantic definition style
Summary: FTP-able bibliography for action semantics
Keywords: action semantics, bibliography, ftp

In article <[e-mail]>, moreaux@litsun22 (Michel Moreaux) writes:
>Here is another reference:

>@INPROCEEDINGS  { M:345,
>     AUTHOR    = "Mosses, Peter D.",
>     TITLE     = "Unified Algebras and Action Semantics",
>...
>     YEAR      = "1989",
> ...
>_Michel Moreaux

Thanks.  That was, however, a somewhat tentative paper, exploring the
use of unified algebras (an unorthodox order-sorted specification
framework, allowing sort union and other operations on sorts) in
action semantic descriptions.  The `official' version of the action
semantics framework, which David Watt and I describe in our respective
books, doesn't rely quite so much on the novel features of unified
algebras.  (For those familiar with the referenced paper: the
combinator for binary choice `A1 or A2' now returns an *individual*
action, rather than the sort union `A1 | A2'.  Thus the nondeterminism
only appears during action performance, not in the actions per se.
However, primitive actions can still be applied to sorts of data,
e.g., `choose a number'.)

Chapter 19 of my book provides an almost up-to-date bibliography of
reports on action semantics.  The current version of the bibliography
can be retrieved by anonymous FTP from ftp.daimi.aau.dk in the
directory pub/action/bibliography.  The README file says:

[This is ftp.daimi.aau.dk:pub/action/bibliography/README]

The bibliography directory contains sources for the Action Semantics
bibliography, as follows:

The file abstract.bib contains all the abstracts from Chapter 19 of
the AS book, together with the abstracts of some recent reports.

The file action.bib contains the same as abstract.bib, except that the
abstracts are omitted.

The files new-abstract.bib and new-action.bib consist of just the
recent entries in abstract.bib and action.bib.

To print the file *.bib, use LaTeX, then BibTeX, then LaTeX again on
the corresponding *.tex file.  N.B.  The ones with abstracts use my
nonstandard bibliography style file alpha-abstract.bst, which allows
longer strings than the standard styles.  (The file old-abstract.bst
could be used instead - it uses the citation keys as labels, like the
widely available abstract.bst.)

The *.dvi files are also available, for those who don't need the
sources.

Finally, the file all.tar.Z contains a compressed tar archive of all
the files.

...

--
Peter D. Mosses | Computer Science Department | <[e-mail]>
~~~~~~~~~~~~~~~ | Aarhus University           | Phone: [phone]
                | Ny Munkegade, Building 540  | Fax:   [phone]
                | DK-8000 Aarhus C,  Denmark  | Telex: 64767 aausci dk