🚀 go-pugleaf

song@minster.york.ac.uk writes:

>I am aware that there are four different styles to define semantics.
>	operational
>	denotational
>	algebraic 
>	axiomatic
>Could anyone give some comments on the following questions:
>	what is the relations among these semantics,
>	what is the purpose of each, 
>	any references on them
>	what is semantics defined in the CSP book

>Many thanks,

>Ji,

OK,

Firstly I have found the following to be useful references in
this particular area.

[Ada, 1980] "The Formal Definition of the Ada Programming Language", Honeywell Inc., 1980.
.XP
[Backus, 1960] "The Syntax and Semantics of the Proposed international Algerbraic Language of the Zurich ACM-GAMM
Conference", \fIInformation Processing\fP, UNESCO, Paris, pp. 125-132, 1960.
.XP
[Chomsky, 1959] "On Certain Formal Properties of Grammars", \fIInformation and Control\fP, \fI2\fP, pp. 137-167,
1959.
.XP
[Donahue, 1976] "Complimentary Definitions of Programming Language Semantics", Lecture Notes in Computer Science,
No. 42, Springer-Verlag, New-York, 1976.
.XP
[Dunlop et al., 1982] "A Comparative Analysis of Functional Correctness", ACM Computing Surveys, \fI14\fP, 2, pp.
229-244, 1982. 
.XP
[Gordon, 1979] "The Denotational Description of Programming Languages, An Introduction, Springer-Verlag, New-York,
1979.
.XP
[Hoare et al., 1973] "An Axiomatic Defintion of the Programming Language Pascal", \fIActa Informatica\fP, \fI2\fP,
pp. 335-355, 1973.
.XP
[Hoare et al., 1974] "Consistent and Complementary Formal Theories of the Semantics of Programming Languages",
\fIActa Informatica\fP, \fI3\fP, pp. 135-153, 1974.
.XP
[Lucas et al., 1969] "On the Formal Defintion of PL/I", \fI Ann. Rev. Auto. Prog.\fP, \fI6\fP, 3, pp. 105-182,
1969.
.XP
[Marcotty et al., 1976] "A Sampler of Formal Definitions", ACM Computing Surveys, \fI8\fP, 2, pp. 191-275, 1976.

Can I offer the following text as a description to the background and use of
theses formal semnatic methods. (Flame away). Honestly, I would appreciate
comments on this text. I used this in a report about a year ago (so I am not sure
that I would agree 100%, but I think it is not bad as a starter!). Comments ?  

.NH
Theoretical Models

.LP
The design and implementation of programming languages illustrates the complex interaction of theory and practice.
Many early language designs grew out of practical needs, with little or no input from theory. However, the
successes and failures of the early programming languages led to some early formal models of programming language
syntax and semantics, which in turn spawned better programming languages. These newer languages still contained a
number of design and implementation errors which required yet better theoretical models. Detailed below is a precis
of some of the major theoretical models that have had a significant impact upon the design and practice programming
languages.
.LP
It may be stated that theoretical models fall into two categories, namely qualitative or quantitative. Theoretical
models may be \fIqualitative\fP or \fIconceptual\fP, describing practice in terms of an underlying set of basic
concepts with not attempt made to provide any formal mathematical description of those concepts. Alternatively,
theoretical models may be \fIquantitative\fP or \fIformal\fP, describing practice in terms of a precise
mathematical model that can be studied, analyzed and manipulated using a series  of mathematical tools. A number of
formal models have been proposed for describing individual aspects of languages and their respective
implementations. A number of these theoretical models are described below.

.NH2
Formal grammars

.LP
The area of programming language design and implementation to receive some of the earliest attention was that of
syntax and translation. Within this area the class of theoretical models that have proved to be most useful are
defined as formal grammars. The BNF grammar is an example of a formal grammar. BNF consists of a set of productions
or grammar rules that recursively define a set of valid character sequences. The BNF grammar model was developed by
Backus and Naur for the description of the syntax of the ALGOL 60 programming language [Backus, 1960]. 

Another formal grammar was developed by the linguist Chomsky [Chomsky, 1959]. He developed a hierarchy of four
types of formal grammar, of which the context-free grammar bears a significant resemblance to the BNF grammar.
Another grammar, the regular grammar, was simpler than the BNF but however was unable to represent as complex a set
of constraints. However, the context-sensitive and unrestricted grammars developed by Chomsky were able to express
constraints that were beyond the ability of the BNF. 

Following Chomksy's pioneering work, numerous other formal grammars were developed, each exploring a different way
of defining the sort of constraints needed for actual programming languages. The context-sensitive and unrestricted
grammars, whilst being more powerful that BNF, turned out to be incorrect models for programming languages. Many
recent grammar forms have been developed in an attempt to overcome the limitations of these previous forms.

In practice, the description of the syntax of a new programming language is always routinely made using a formal
grammar. Most commonly some variant of BNF grammar is used for the definition, but often a more powerful form,
called a two-level grammar, is used. Theoretical studies have clarified the limits of BNF grammars and hence it is
now commonly understood that some classes of syntactic constraints cannot be described with them. Often, these are
described via attaching some informal notes to a BNF. The users of a language now routinely use a formal grammar to
answer questions about syntax. Implementors of a language also routinely use a formal grammar to generate a parser
for the language.

.NH2
Problems in Semantics

.LP
The definition of semantics in most programming language manuals is given in ordinary prose. In order to define the
syntax of a construct a production from a BNF or other formal grammar is provided. Added to this formal syntax is a
few paragraphs and (hopefully) a number of examples to define the semantics. Unfortunately it has been the case,
that the prose is ambiguous in meaning leading to different interpretations of the semantics of a language
construct. The consequences of such problems include may affect both programmer and implementor. Firstly, a
programmer may misunderstand what the program will do when executed and also an implementor may implement a program
construct in a manner different from other implementors of the same programming language. Hence, as with syntax,
methods are required to provide a precise, readable and concise definition of the semantics of a programming
language.

The problem of semantic definition has been a research topic for a considerable period. However, unlike the area of
syntactical definition, satisfactory solutions have been rare. Many different methods of formal definitions have
been developed and these may be subdivided into three general classes :-
.RS
.IP \(bu
Operational Methods
.IP \(bu
Denotational or Functional Methods and 
.IP \(bu
Axiomatic Methods.
.RE

.LP
\fBOperational methods\fP
.LP
An operational definition of a programming language is a definition organized around a formal model of how programs
in the language are executed on a virtual computer. It corresponds to an abstraction from the viewpoint of how the
language is implemented. The Vienna Definition Language is an example of an operational approach.

\fBDenotational methods\fP
.LP
A second class of semantic definition methods attempt to directly construct a definition of the function that each
program computes. The definition is built up hierarchically through definition of the function computed by each
individual program construct. Ultimately, a complete functional model of an entire program may be derived. The
method of \fIdenotational semantics\fP and the method of \fIfunctional semantics\fP are examples of this approach.

\fBAxiomatic methods\fP
.LP
A third class of methods for semantic definition define the semantics of each syntactic construct in the language
directly by giving an axiom or rule of inference that may be used to deduce the effect of execution of that
construct. In order to understand the meaning of an entire program it is necessary to use the axioms and rules of
inference in manner similar to ordinary proofs within the area of mathematics. The method of \fIaxiomatic
semantics\fP is an example of this method.

.NH3
Discussion

.LP
The various alternative semantic definition methods within each of these classes have provided the basis for
extensive formal study of issues relating to programming language semantics. The work of program correctness proofs
has been closely associated with the development of axiomatic semantics. Denotational semantics have provided the
basis for a deeper sense in which a program computes a function. Finally, operational semantics have led to
discovery of subtle issues in language implementations that are often not apparent to the language implementors.
semantic definition studies upon ition of most of Pascal is given by Hoare and Wirth [1973]. Donahue [1976] and
ml semantic definitions are becoming more an accepted part of the definition of new programming languages. One of
the requirements imposed during the definition of Ada was that a formal semantic definition was required for Ada.
The operational formal definition of PL/I was used as the basis for the standard PL/I definition; although it
should be added that the formal notation was not eventually retained within the standard. The effect of formal
semantic definition studies upon theoretical models of programming languages has not been as great as the effect of
formal grammars upon the definition of syntax. 

No single semantic definition method has been found useful for both user and implementor. The operational methods
often provide good formal models of implementation, but the definitions are often too detailed to be of value to an
user. Denotational methods do not provide much guidance to the implementor and have usually proven too complex to
be of direct value to the users. Axiomatic methods are more directly understandable by the language user, but
generally it has been found that they cannot be used to completely define a language without the definition
becoming extremely complex; providing little guidance to the implementor.

To date, the major impact of semantic definition of programming languages has been the use of such a definition
during the design of a language to detect and clarify subtle points that might lead to ambiguities in the language
definition. It should be noted however, that the final definition is still ordinarily presented using prose. The
denotational semantic definition of Ada was found to play a significant role in the development of the programming
language, yet only English prose and a BNF grammar are utilised to present the language formally.

.NH3
Literature

.LP
Marcotty et al. [1976] survey the issues relating to formal semantic definition and describe several methods.
Gordon [1979] provides an good introduction to denotational semantics. Dunlop and Basili [1982] describe Mills
functional semantics and contrast and compare it with denotational semantics. Lucas and Walk [1969] describe the
operational method called the Vienna Definition Language that was used for the formal definition of PL/I. A
denotational semantic definition of most of Ada is given in [Ada, 1980] and an axiomatic definition of most of
Pascal is given by Hoare and Wirth [1973]. Donahue [1976] and Hoare and Lauer [1974] contrasts these various
approaches and recommend a combination of equivalent definitions, each used for different purposes. 
Hoare and Lauer [1974] contrasts these various approaches and recommend a combination of equivalent definitions,
each used for different purposes.

Happy reading. Hopefully there are some pointers in there for you.

Regards

Brian

Brian J. King           | Voice: +44 91 222 8557  Fax: +44 91 261 1182  
Engineering Design Centre      | JANET: B.J.King@uk.ac.ncl 
The University          | Internet:B.J.King%newcastle.ac.uk@cunyvm.cuny.edu
Newcastle upon Tyne NE1 7RU UK | UUCP : ...!mcvax!ukc!ncl.ac.uk!B.J.King

Brian J. King        | Voice: +44 91 222 6000 ext 8558  Fax: +44 91 261 1182    
Engineering Design Centre      | JANET: B.J.King@uk.ac.ncl 
The University           | Internet:B.J.King%newcastle.ac.uk@cunyvm.cuny.edu
Newcastle upon Tyne NE1 7RU UK | UUCP : ...!mcvax!ukc!ncl.ac.uk!B.J.King

In article <720801988.16035@minster.york.ac.uk> song@minster.york.ac.uk 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.

../Dave

In article <DMASON.92Nov5131527@plg.uwaterloo.ca> dmason@uwaterloo.ca (Dave Mason) writes:
   In article <720801988.16035@minster.york.ac.uk> song@minster.york.ac.uk 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

[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 :-

@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}
}

Here is another reference:

@INPROCEEDINGS  { M:345,
     AUTHOR    = "Mosses, Peter D.",
     TITLE     = "Unified Algebras and Action Semantics",
     BOOKTITLE = "Proceedings of the 6th Annual Symposium on Theoretical Aspects of Computer Science, STACS'89",
     ADDRESS   = "Paderborn, FRG",
     MONTH     =  feb,      
     YEAR      = "1989",
     SERIES    = "Lecture Notes in Computer Science",
     VOLUME    = "349",
     PUBLISHER = "Springer-Verlag",
     PAGES     = "17-35"}

_Michel Moreaux
--
------------------------------------------------------------------------------
Michel Moreaux,                           | "Ceux qui ne savent rien en savent
Ecole Polytechnique Federale de Lausanne  |  toujours tout autant que ceux qui
Departement d'Informatique                |  n'en savent pas plus qu'eux"
Laboratoire d'Informatique Technique      |                  P. Dac.
EL-Ecublens                               |___________________________________
CH-1015 Lausanne                           
Phone # : (21) 693-46-72,   e-mail : moreaux@litsun.epfl.ch
------------------------------------------------------------------------------

In article <MOREAUX.92Nov9161246@litsun22.epfl.ch>, 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 | <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

In article <720801988.16035@minster.york.ac.uk> song@minster.york.ac.uk writes:

>I am aware that there are four different styles to define semantics.
>	operational
>	denotational
>	algebraic 
>	axiomatic

First, so called `axiomatic' semantics are an unfortunate misclassification
of a proof system as a style of semantics.

One of the primary objectiv of semantics is to allow us to formalize the
intuitive notion of correctness of a program. We then have meaningful
basis for discussions of questions about various validation schemes
such as the adequacy of a proposed testing scheme or the soundness of
a proof system or the (relative) completeness of a proof system, etc.

Our muddling together of the notions of correctness and provability
is not, I suppose, too surprising in light of the fact that a clear
recognition of this distinction in mathematics awaited the development
of model theory in the 1940's.

>Could anyone give some comments on the following questions:
>        what is the relations among these semantics,
>        what is the purpose of each,

Another primary objective of semantics is to define formally for users
precisely what they can expect a program will do in all possible
situations. To meet this objective, operational semantics are a very
tempting approach. They generally can be viewed as defining some sort of
automaton and reducing the problem of giving semantics for the programming
language to one of translating the high level language programs into
programs for the automata and then using the usual sequence of states
(computational history) semantics which are the norm when supplying
semantics for automata. The intermediate automata usually have a simpler
and more appropriate architecture than say a 68000 presents. but the
idea is still roughly to explain the semantics of a program by examining
what happens when you compile it for a machine with a really nice
architecture. This implementation oriented approach could be expected
to communicate better with programmers.

A third major objective of semantics is to define formally for
implementors precisely what effect their compilers/interpreters are
supposed to produce under all circumstances. This is the objective
which seems to favor denotational semantics. Denotational semantics
are explicit semantics, as opposed to the implicit semantics which result
from the operational approach. I.e., operational semantics produce a
welter of irrelevant information (computational histories), from which the
essential information (the input/output pairs, in the case of sequential
programs) must be extracted. If, for example, a compiler writer has a
target architecture that is wildly different from that of the automaton
used in the operational semantics for his source language or even if
he's just writing a highly optimizing compiler, he's got a real problem
in relating the computational histories his output code will produce
to those described by the semantics. Denotational semantics address this
problem by attempting to produce minimalist semantics which tell the
compiler writer exactly the effect his compiled code should produce and
nothing more. The main drawback of this Spartan approach seems to be
that, of necessity, it leads us into such unfamiliar topics as minimal
fixed points, etc. and thereby makes it more difficult to meet the other
two primary objectives of semantics.

Now algebraic semantics would seem to be predicated on the dubious
proposition that computation is entirely describable within a limited
first-order subarea of mathematics -- namely algebra.

-- 

/Bill

In article <1992Nov11.195443.23006@cis.ohio-state.edu>, ogden@seal (William F Ogden) writes:

>Another primary objective of semantics is to define formally for users
>precisely what they can expect a program will do in all possible
>situations. To meet this objective, operational semantics are a very
>tempting approach. They generally can be viewed as defining some sort of
>automaton and reducing the problem of giving semantics for the programming
>language to one of translating the high level language programs into
>programs for the automata and then using the usual sequence of states
>(computational history) semantics which are the norm when supplying
>semantics for automata. The intermediate automata usually have a simpler
>and more appropriate architecture than say a 68000 presents. but the
>idea is still roughly to explain the semantics of a program by examining
>what happens when you compile it for a machine with a really nice
>architecture. This implementation oriented approach could be expected
>to communicate better with programmers.

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.

>A third major objective of semantics is to define formally for
>implementors precisely what effect their compilers/interpreters are
>supposed to produce under all circumstances. This is the objective
>which seems to favor denotational semantics. Denotational semantics
>are explicit semantics, as opposed to the implicit semantics which result
>from the operational approach. I.e., operational semantics produce a
>welter of irrelevant information (computational histories), from which the
>essential information (the input/output pairs, in the case of sequential
>programs) must be extracted. 

But the denotations of statements, declarations, etc., are not I/O
relations!  They necessarily deal with *auxiliary* entities, such as
environments and stores, whose relevance to particular implementations
is not nearly so direct as that of the I/O relation.  Moreover, to
model interleaving (i.e., unspecified order of evaluation in the
presence of side-effects) one uses so-called `resumptions' as
denotations; these are very closely related to computations.  It seems
that one cannot get `fully abstract' denotations for such constructs.

>If, for example, a compiler writer has a
>target architecture that is wildly different from that of the automaton
>used in the operational semantics for his source language or even if
>he's just writing a highly optimizing compiler, he's got a real problem
>in relating the computational histories his output code will produce
>to those described by the semantics. Denotational semantics address this
>problem by attempting to produce minimalist semantics which tell the
>compiler writer exactly the effect his compiled code should produce and
>nothing more. 

The trouble is that this effect is `encoded' as intricate compositions
of pure, higher-order functions, which can be quite difficult to
relate to an intended implementation.  Similar problems arise if one
tries to use concurrent processes as denotations, instead of
functions: one ends up losing sight of the *concepts* of the described
language, which involve scopes, variable allocation, assignments,
sequencing, etc. (as well as functions and processes, of course).

>The main drawback of this Spartan approach seems to be
>that, of necessity, it leads us into such unfamiliar topics as minimal
>fixed points, etc. and thereby makes it more difficult to meet the other
>two primary objectives of semantics.

The use of minimal fixed points is neither more nor less difficult to
explain than that of recursive (i.e., self-calling) procedures.
Readers of semantic descriptions don't usually need to understand
*why* things with certain desirable properties exist.  In fact in the
mid '60s, Strachey was happily using minimal fixed point operators in
denotational descriptions, long before the existence of a mathematical
model for them was shown!

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.

>Now algebraic semantics would seem to be predicated on the dubious
>proposition that computation is entirely describable within a limited
>first-order subarea of mathematics -- namely algebra.

- which can specify Turing machine computations, and hence is
universal.  In any case, there are `first-order' models for domains,
e.g., Scott's P-omega model, where continuous functions are
represented by their approximation graphs.

-- 
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

In article <1992Nov13.084826.26088@daimi.aau.dk> pdm@daimi.aau.dk (Peter D. Mosses) writes:
>In article <1992Nov11.195443.23006@cis.ohio-state.edu>, ogden@seal (William F Ogden) writes:
>>Now algebraic semantics would seem to be predicated on the dubious
>>proposition that computation is entirely describable within a limited
>>first-order subarea of mathematics -- namely algebra.

I assume you mean "univeral algebra", and not "algebra" as mathematicians
generally use the word. 

>- which can specify Turing machine computations, and hence is
>universal.  In any case, there are `first-order' models for domains,
>e.g., Scott's P-omega model, where continuous functions are
>represented by their approximation graphs.

In any event, I've never been able to understand the virtue of working 
within a mathematical model of computation which permits description of
processes that cannot be carried out, even in principle, by any physical
computing device. What is it that one intends to learn by application of
these methods?


>
>-- 
>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


-- 


yodaiken@chelm.cs.umass.edu

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.'

Moreover, it does seem likely that, whenever we finally discover
an appropriate set of language constructs to handle concurrency cleanly,
their denotational semantics will probably involve something comparable to
the state sequence notion which shows up in operational semantics.

   ...

>The use of minimal fixed points is neither more nor less difficult to
>explain than that of recursive (i.e., self-calling) procedures.
>Readers of semantic descriptions don't usually need to understand
>*why* things with certain desirable properties exist.  In fact in the
>mid '60s, Strachey was happily using minimal fixed point operators in
>denotational descriptions, long before the existence of a mathematical
>model for them was shown!

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_.

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.

>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.
-- 

/Bill

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

pdm@daimi.aau.dk (Peter D. Mosses) writes:

>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:
>>   ...

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

Continue here please.

I am sure there are many people who want to see such discussions.
I am one of them.

PR
--
Piotr (Peter) Rudnicki

In article <piotr.722190155@sedalia>, piotr@cs (Piotr Rudnicki) writes:
>pdm@daimi.aau.dk (Peter D. Mosses) writes:
>>[Perhaps we should continue this by e-mail, as it probably doesn't
>>have sufficient general interest for comp.specification.]
>
>Continue here please.
>
>I am sure there are many people who want to see such discussions.
>I am one of them.
>
>PR
>--
>Piotr (Peter) Rudnicki

Many thanks for the encouragement!  I also received several e-mail
messages expressing similar views.  I'll be happy to continue the
discussion of semantics on comp.specification - and others should feel
free to join in, of course... with questions, as well as opinions.

Just let me add a bit of explanation, followed by a perhaps somewhat
provocative statement.

Some of you may be aware that I studied denotational semantics with
Strachey in Oxford, developed a Semantics Implementation System (SIS)
for denotational semantics, and more recently wrote a chapter on the
approach for the Handbook of Theoretical Computer Science (ed. Jan van
Leeuwen, Elsevier, 1990).  You may be puzzled that I've been pointing
out problems with the denotational approach, and advocating another,
more operational approach, namely action semantics (references
provided in an earlier message - mail me if you missed that one).

Actually, I still think that denotational semantics is useful - but
only for dealing with small-scale, unrealistic languages, of the kind
often used as examples in textbooks on semantics.  The main pragmatic
problem is it doesn't seem to *scale-up* smoothly - not even as far as
medium-scale languages like Standard Pascal.  It becomes very heavy,
rather like writing large (functional) programs without any
modularity.

I'd like to make a distinction: between the *concepts* underlying the
usual denotational semantics of programming languages, and the
*representation* of these concepts by higher-order functions on Scott
domains.  In my view, it's only the latter (together with the use of
lambda-notation) that causes the pragmatic problems of denotational
semantics.  The concepts themselves, developed primarily by Strachey,
Burstall, and Landin, are useful *whatever* semantic framework one
uses!  For example, the distinction between bindings and storage
(symbol tables and memories, environments and states) is crucial for
any sensible semantic description of passing parameters by reference.
Action semantics provides straightforward notation for such concepts,
rather than representing them all in terms of higher-order functions.

Finally, to be a bit provocative :-) let me claim that if one is
making a denotational semantics of a simple language, and wants to
make the semantic equations independent of whether the model is in the
direct or in the continuation-passing style (i.e., hiding
information), one is *forced* to introduce auxiliary notation akin to
action notation!  Just contemplate the semantic equation for statement
sequencing...

-- 
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

In article <1992Nov20.085655.8721@daimi.aau.dk>, 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: pdm@daimi.aau.dk (Peter D. Mosses)
Subject: Re: Semantic definition style
Summary: Action semantics is best :-)
Keywords: action semantics, action notation, denotational semantics,
	operational semantics

In article <BEVAN.92Nov7140134@hippo.cs.man.ac.uk>, bevan@cs (Stephen J Bevan) writes:
>In article <DMASON.92Nov5131527@plg.uwaterloo.ca> dmason@uwaterloo.ca (Dave Mason) writes:
>   In article <720801988.16035@minster.york.ac.uk> song@minster.york.ac.uk 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: pdm@daimi.aau.dk (Peter D. Mosses)
Subject: Re: Semantic definition style
Summary: FTP-able bibliography for action semantics
Keywords: action semantics, bibliography, ftp

In article <MOREAUX.92Nov9161246@litsun22.epfl.ch>, 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 | <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