[TYPES] Terminology in operational semantics

[Roy L. Crole]

Johan Glimming <glimming at kth.se> writes:

> I am confused by what I think appears to be different notions of
> operational semantics. Nielson-Nielson seems to distinguish natural
> semantics from structural operational semantics, whereas Winskel
> considers (in a remark) natural semantics one particular notion of
> structural operational semantics. Also we have big step semantics
> versus small step semantics.
> On the other hand, some researchers distinguish  between reduction
> semantics and operational semantics, and I am not clear about how this
> relates to the above notions, if at all.

A fair question. I've made a few comments below which I hope might be
helpful. The bottom line seems to be that there is indeed conflicting
terminology present in the literature, and thus in any self-contained
situation (paper, book etc) you should make your definitions clear and
stick to them!

I usually use the term "structural operational semantics" (SOS) to refer to
a 'semantics' given to a programming language (typically) using rules

                H1 H2 ....... Hn 
              ------------------- LABEL(P) 
                        C 
 
specifying an inductive definition. In any (valid) deduction tree, the
instance of each rule within the tree (LABEL(P) above) is determined
by the 'structure' (abstract syntax tree) of a program P occurring in
the conclusion C of the instance (eg C might be P => V for Big Step
Semantics). 'Operational' refers to the fact that the semantics can be
seen to be *directly* related to a (high-level) implementation or
'operational' behaviour, rather than by *reference* to some sort of
additional or external model (as in denotational semantics).

Many people use "Natural Semantics" and "Big Step Semantics"
essentially interchangeably. The rule above is supposed to be an
example; C might be (8+7)*1 => 15. 'Big Step' simply refers to the
complete evaluation of a program P to a final value V.  'Natural' is
referring to natural deduction. In this style of presentation, rules
and deductions are similar to those found in natural deduction
presentations of logic (sets of logical hypotheses are mirrored (eg)
by environments for variables; and the discharge of a hypothesis is
mirrored (eg) through binding):


              E, x -> 4 |- P2 => V2
                      E |- P1 => 4 
           -------------------------------
              E |- Let x = P1 in P2 => V2

In this sense, natural semantics is an example of SOS, (as in Glynn's
book). 

Many people use "Reduction Semantics" and "Single Step Semantics"
essentially interchangeably. Both names are indicative of the more
fine grained computation 'steps', or 'reductions' seen in examples
such as

          (8+7)*1 --> 15*1 --> 15 

Finally, these are rather general observations, and when considering
the complexities of real programming languages it is often quite
possible to quibble with them; the comments above are of course not
robust definitions.

Roy Crole.