NetNews Usenet Archive 1992 #26/NN_1992_26.iso/spool/comp/specific/529

Text File | 1992-11-13 | 6.1 KB | 113 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] (William F Ogden)
Message-ID: <[e-mail]>
Summary: not a word about action semantics :-)
Keywords: structural operational semantics, denotational semantics
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]>
Date: Fri, 13 Nov 92 08:48:26 GMT
Lines: 97

In article <[e-mail]>, 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 | <[e-mail]>
~~~~~~~~~~~~~~~ | Aarhus University           | Phone: [phone]
                | Ny Munkegade, Building 540  | Fax:   [phone]
                | DK-8000 Aarhus C,  Denmark  | Telex: 64767 aausci dk