Article View: comp.specification
Article #265Re: Semantic definition style
From: Peter D. Mosses
Date: Fri, 13 Nov 1992 08:48
Date: Fri, 13 Nov 1992 08:48
97 lines
6340 bytes
6340 bytes
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
Technical Details
Message-ID:
<1992Nov13.084826.26088@daimi.aau.dk>Path:
arc1-ca.pugleaf.net!sparky!uunet!mcsun!sunic!dkuug!daimi!pdmReferences:
<720801988.16035@minster.york.ac.uk> <1992Nov11.195443.23006@cis.ohio-state.edu>Show Full Headers
Complete Article Headers
Newsgroups: comp.specification Path: arc1-ca.pugleaf.net!sparky!uunet!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: <1992Nov13.084826.26088@daimi.aau.dk> Summary: not a word about action semantics :-) Keywords: structural operational semantics, denotational semantics 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> Date: Fri, 13 Nov 92 08:48:26 GMT Lines: 97