🚀 go-pugleaf

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