[PRL] den sem
William D Clinger
will at ccs.neu.edu
Thu Mar 1 14:43:17 EST 2007
A Brief Introduction to Denotational and Operational Semantics
(Extended Abstract)
by William D Clinger
Part 1
NU PRL, 1 March 2007
First I'd like to thank Matthias and Mitch for inviting
me to talk to you about this fascinating subject.
I endorse Mitch's introductory remarks and will add
rather too many of my own, drawing several distinctions
between my understanding of the subject and Matthias's.
Here's an abstract of my talk:
Regarding denotational and operational semantics:
1. Both can be formal.
2. Both can be executable.
3. Neither has to be executable.
Here's an outline of my talk:
Part 1:
philosophical preliminaries
denotational versus operational
toy examples demonstrating claims 1 and 2
nontermination
another example demonstrating claims 1 and 2
compiler correctness
full abstraction
Part 2:
Matthias's example (demonstrating claims 1, 2, 3)
nondeterminism
denotational and operational semantics
of first order logic
non-executable semantics for first order logic
executable semantics for first order logic
clarification of Matthias's points
conclusions
* * *
Philosophical Preliminaries
===========================
Semantics is about the meaning(s) of language. It is
a philosophical subject. During the 19th and 20th
centuries, semantics became a primary focus of logicians
and linguists, whose results on the semantics of formal
languages provided both philosophical and pragmatic
foundations for mathematics and computer science.
Semantics is the bridge between two important notions:
* what it means for a function to be computable
* what it means for a formal system to be executable
Church's unprovable but apparently true thesis can be
stated as follows: A function is computable if and only
if it is the meaning of a certain kind of executable
formal system. One of the reasons we believe Church's
thesis is its robustness: You can take the executable
systems to be Turing machines, or While programs, or
programs written in a functional subset of Scheme or
any of a thousand other languages, and your choice of
executable systems doesn't affect the meaning of Church's
thesis. Even if Church's thesis were someday falsified
(as could conceivably happen, because it is essentially
an empirical fact), something interesting is going on
here.
We'll need to be careful about the words "computable"
and "executable", because they are commonly used in two
different ways:
* to talk about total functions and programs that
always terminate
* to talk about partial functions and programs that
might not terminate
It is all too easy to use one of those words to mean one
thing, and then to turn around and use it to mean the
other. Doing so in the statement of a theorem, proof,
or argument is a fallacy we must learn to recognize.
We will also need to be careful about "effective" and
"representation". "Effective" is almost a synonym for
"computable" and "executable", but is more constructive
(or intuitionistic): a thing may be computable in the
classical sense (perhaps because you can come up with
some kind of nonconstructive proof that a set is finite)
without being effectively computable (because you have
no idea how to go about enumerating the set's elements).
Representations are the only things with which we can
compute. We have to be careful about them because we
want the correspondence between representations and the
things they represent to be effectively computable, and
that there is a philosophical concept of considerable
subtlety.
Denotational versus Operational
===============================
Denotational semantics is based on the old philosophical
idea that nouns, verbs, adjectives and so forth denote
things, actions, qualities, and so forth, and that the
meanings of sentences, paragraphs, and the great American
novel can be constructed by composing these denotations
as directed by the structure of the sentence, paragraph,
or novel.
For formal logics and programming languages, mathematical
functions often serve as denotations.
Operational semantics is more likely to regard the meaning
of a proposition or program as a description of proofs or
computations.
The denotation approach therefore feels closer to the
function side of Church's thesis, while the operational
approach feels closer to the executable formal system
side.
Don't let that feeling mislead you into thinking that
denotational semantics is always about functions and
can't be executable, or that operational semantics is
never about functions and is always executable. The
main purpose of my talk is to provide counter-examples
to those misconceptions.
Toy Examples
============
When approaching a difficult subject, it is a good idea
to start with some of the simplest possible examples.
We will therefore begin with the two languages I call
BOOLEAN and CONJUNCTION.
(The main danger of simple examples is that they aren't
likely to reveal the true complexity of the subject, so
you might be tempted to jump to the premature conclusion
that you understand the subject better than you do. My
advice is: Don't jump. We'll get around to realistic
examples later.)
The BOOLEAN language contains only two programs:
BOOLEAN ::= true | false
To develop a denotational semantics for BOOLEAN, we have
to decide on the denotations. Let's say that programs
in this language will denote the number 1 or the number 0.
Our denotational semantics of a BOOLEAN program is given
by the semantic function B: BOOLEAN --> {0,1} defined by
B(true) = 1
B(false) = 0
I hope you will agree that this is a reasonably formal
semantics, and that it is also executable. If anyone
objects to either, I will simply rephrase my statement
of the semantics in a more formal and more obviously
executable language, such as a functional subset of
Scheme:
; B: {true, false} --> {0,1}
;
; Given a BOOLEAN program (represented as a symbol),
; returns its denotation (represented as a number).
(define (B pgm)
(case pgm
((true) 1)
((false) 0)))
Anyone who claims that the definition of B above is not
formal or not executable may leave the room now.
The above semantics is denotational, which establishes
the first half of my first two claims. I have not yet
established that an operational semantics can be formal
or executable, but I'll get to that eventually.
First I want to describe a denotational semantics for a
language with infinitely many programs:
CONJUNCTION ::= BOOLEAN | BOOLEAN & CONJUNCTION
Our denotational semantics of a CONJUNCTION program is
given by the semantic function C: CONJUNCTION --> {0,1}
defined by
C(b) = B(b)
C(b & c) = B(b) * C(c)
where * indicates ordinary multiplication. To put it
even more formally:
; C: CONJUNCTION --> {0,1}
;
; Given a CONJUNCTION program represented as described
; by the grammar
;
; CONJUNCTION --> BOOLEAN
; | (& BOOLEAN CONJUNCTION)
; BOOLEAN --> true | false
;
; returns its denotation (represented as a number).
(define (C pgm)
(cond ((symbol? pgm)
(B pgm))
(else (* (B (cadr pgm)) (C (caddr pgm))))))
Once again, this denotational semantics is both formal
and executable.
Now let's look at a conventional big-step operational
semantics for CONJUNCTION:
true --> 1
false --> 0
b --> i
c --> j
k = i * j
-----------
b & c --> k
We aren't done yet, because we haven't yet described
how the meaning of a CONJUNCTION program is related to
those inference rules. There are two obvious choices
for the operational meaning of a CONJUNCTION program c:
* c means the set of all k such that c --> k
* c means the set of all proof trees whose consequent
is c
That choice is a source of power, because most of our
operational semantics (i.e. the entire set of inference
rules) is independent of that choice. We can interpret
the inference rules as the specification of a relation
that relates programs to their denotations, or as the
specification of a relation that relates programs to
their computations. Whichever is more convenient. We
can have our cake and eat it too.
If we take the operational meaning of c as the set of
all k such that c --> k, it is easy to prove that the
operational meaning coincides with the denotational.
Whenever convenient, we can take the operational meaing
of c to be a set of proof trees. We can have our cake
and eat it too.
The ability to interpret a semantics in two or more ways
is not just a source of power. It is also a source of
confusion, against which we must guard.
We could also prove that the denotational semantics of
CONJUNCTION is fully abstract, which means that c1 and
c2 are interchangeable in all contexts if and only if
they have the same denotation.
It is not hard to extend these ideas to a COMBINATIONAL
language that describes an economically important and
theoretically interesting class of circuits. We could
also call that language PROPOSITIONAL, since it is
isomorphic to propositional logic.
Nontermination
==============
When we go from combinational to sequential circuits,
or from propositional logic to first order logic, or
from primitive recursion to general recursion, or from
certain special-purpose programming languages to fully
general-purpose programming languages, we have to be
more careful about our philosophical words: computable,
executable, effective, representation.
With general recursion or general-purpose programming
languages, we will have to deal with so-called partial
functions as well as with total functions. In other
words, some programs won't terminate on all legal
inputs. Since the halting problem is recursively
undecidable (and is therefore undecidable period if
Church's thesis is true), we can't tell (in general)
which programs won't terminate on which inputs.
If we insist upon a semantics that tells us which
programs don't terminate on which inputs, then our
semantics won't be computable, which means it won't
be effective at telling us what we insist it tell us.
We have two choices:
* use a non-effective (non-computable, non-executable)
semantics
* don't insist upon a semantics that tells us which
programs won't terminate on which inputs
Both of those choices are viable, and can be sensible
depending on your purpose for the semantics. When we
are describing the semantics of a programming language,
we generally want our semantics to be effectively
computable. That is, we want our semantics to be in
executable form, or easily and effectively transformable
into executable form.
To obtain an executable semantics, we must accept that
the semantics won't tell us which programs won't
terminate on which inputs. We'll have to content
ourselves with a semantics that tells us which programs
do terminate on which inputs.
If that's all we ask, then we can design an executable
semantics. It can be denotational, or it can be
operational.
The WHILE Language
==================
The set of WHILE programs is generated by:
P --> input I; Q; output E
Q --> S | S; Q
S --> skip
| I := E
| if B then S else S
| while B do S
| begin Q end
E --> I | N | ( E )
| E + E | E - E | E * E | E / E
B --> not B | E < E | E = E | E > E
where I and N are nonterminals that generate identifiers
and natural numbers, respective.
Many textbooks show how to define denotational and
operational semantics for languages like WHILE, so
I don't need to show the details here. My concern
is to show that the first two claims of my abstract
hold even for the semantics languages like WHILE,
and to highlight the important philosophical and
technical points. For full details, I recommend
the Nielson's book [1].
In chapter 2, the Nielsons present a big-step natural
semantics that defines a relation of the form
<stmt, state> --> state
That relation can be used to define an input/output
relation of the form
<p, number> --> number
where p is any WHILE program.
To talk about non-termination, it helps to have a
symbol for it. The conventional symbol for it is
an upside-down T, sometimes pronounced "tack", but
more meaningfully pronounced "bottom". I'll write
it as \bottom. For any set A, let's define
A_\bottom = A \union {\bottom}
Definition. The partial function computed by p is
f_p: N --> N_\bottom defined by
f_p(n) = k if <p, n> --> k
f_p(n) = \bottom otherwise
We have to be extremely careful here. The partial
function f_p computed by p is defined by the above
definition in a non-constructive mathematical sense,
but f_p is not computable when it is regarded as a
total function from N to N \union {\bottom}.
On the other hand, the graph of f_p (i.e. the set
of ordered pairs <n, k> such that <p, n> --> k) is
recursively enumerable. Furthermore, a recursive
enumeration of a partial function's graph can be
used as a representation of the partial function.
The recursive enumeration is computable in the
sense that there exists a Turing machine (or Scheme
program, or what-have-you) that computes it.
The operational semantics of p therefore defines an
effective enumeration of the graph of the partial
function f_p. In other words, it computes a
representation of f_p. If f_p happens to be total,
then the operational semantics happens to define an
effective method of computing f_p(n) for any natural
number n. For some programs, we might be able to
prove that f_p is total, in which case the semantics
gives us an effective method of computing f_p(n).
Even if f_p happens to be total, we probably won't
be able to prove it is total. That means the
semantics is giving us a method for computing f_p(n).
You (but not I) might even say it gives us an
effective method for computing f_p(n). One thing
no one should say, however, is that the operational
semantics effectively gives us an effective method
for computing f_p(n). It does no such thing.
The paragraph above is philosophically subtle. It
would be easy to think the operational semantics is
giving us more than it is.
When we say that the big-step operational semantics
is executable, we mean that it gives us an effective
method for enumerating the graph of the partial
function f_p. That's all that it means.
The Nielsons also present a small-step operational
semantics for WHILE, and prove its equivalence with
the big-step semantics. That means the small-step
semantics is executable in exactly the same sense
as the big-step semantics.
In chapter 4, the Nielsons present a denotational
semantics for WHILE. Their metalanguage could
easily be translated into a functional subset of
Scheme, so their metalanguage is executable. The
Neilsons use that metalanguage to define semantic
functions
S: Q --> (State -->\bottom State)
A: E --> (State --> N)
where (State -->\bottom State) is the set of all
partial functions from states to states. Since
S computes a total function that was defined by
a program written in an executable language, S is
executable.
Remember the power we gained by looking at an
operational semantics in either of two ways?
We can do the same sort of thing with this
denotational semantics. We can regard S as a
mathematical function that translates sequences
of statements into partial functions from states
(which are themselves mathematical functions)
to states, which is all very fine and abstract.
Or, remembering that S is executable, we can
take into account the fact that S operates by
taking a representation of a sequence of states,
and returns a representation of a partial function
from representations of states to representations
of states. This less abstract view is the more
philosophically correct view.
Indeed, S can be viewed as a compiler: given any
sequence of WHILE statements q, S returns a
metalanguage representation of the denotation of
q. If we think of the metalanguage as a functional
subset of Scheme (for such it is, essentially),
then the denotation of q will be represented by a
procedure that takes a state and (if it returns at
all) returns a state.
The function S can be used to define a semantic
function W: WHILE --> (N -->\bottom N) as follows:
W (input x; q; output e)
= \lambda n . A(e)(S(q)[x=n])
To emphasize the executability of this, I'll write
the same thing in an equivalent metalanguage:
(define (W x q e)
(lambda (n)
((A e)
((S q)
(extend-state (empty-state) x n)))))
Now we can define the partial function computed by
a WHILE program p of the form
input x; q; output e
to be (W x q e). Please note that all of this is
effective; it's basically the same sort of thing
that Mitch's interpreters do.
The Nielsons present the basic technical machinery
of fixed point semantics, and use it to prove their
denotational semantics for WHILE is equivalent to
their big-step and small-step operational semantics.
Corollary. For any WHILE program
p = input x; q; output e
the partial function represented by (W x q e) is
mathematically identical to f_p.
Summarizing: All three semantics for WHILE programs
(denotational, big-step, and small-step) are:
* formal
* executable
* equivalent
Compiler Correctness
====================
Everything the Nielsons did for the WHILE language
can be done for lower-level languages as well.
Some years ago (circa 1990) I defined a low-level
language we might call WHILE machine language, or
WML for short. I defined a denotational semantics
for WML, defined a code generation algorithm that
translated WHILE programs into WML, and proved the
translated program was equivalent to the original.
In other words, my compiler was correct.
That proof was not entirely trivial, thanks to the
fixed point operator used to define the semantics
of while loops. It wasn't all that hard, though.
I could have defined an operational semantics for
WML, and proved it equivalent to the denotational
semantics, but didn't have any reason to do so at
the time.
It would be easy to define a denotational semantics
for Turing machines. It would also be easy to
define a big-step or small-step semantics for Turing
machines. (In fact, I almost did so last week when
I wrote a Turing machine interpreter for my CS U390
students to use [2].) Using the Nielsons' technique,
we could then prove equivalence of the denotational
and operational semantics of Turing machines.
Both the denotational and operational semantics of
Turing machines would be formal and executable in
exactly the sense we discussed for WHILE programs.
I could also define a compiler that translates WML
programs into Turing machines. Then I could prove
the correctness of that compiler. Composing the
translation from WHILE to WML with the translation
from WML to Turing machines, I would have a compiler
from WHILE to Turing machines. I would also have
a proof of that compiler's correctness.
Fun, isn't it?
Full Abstraction
================
The ease with which denotations can be composed
makes denotational semantics attractive for proving
the correctness of simple non-optimizing compilers.
Those compilers are usually structured as a simple
composition of translations, whose correctness
follows more or less immediately from correctness
of the individual translations.
(I don't mean to say that it is trivial. Mitch Wand
probably knows at least as much about this as anyone
in the world [3]. He could tell you stories.)
Denotational semantics also works well when proving
the correctness of a few simple optimizations, such
as constant propagation and common subexpression
elimination in purely functional languages.
The denotational approach starts to break down when
optimizations become more complex. The basic problem
is that the more complex optimizations usually depend
upon the fact that the program never does certain
things. Doing things is an operational notion, so
it can be hard even to state the enabling conditions
within a denotational semantics.
This problem is slightly related to the problem of
full abstraction. For a denotational semantics, full
abstraction means that two subprograms p1 and p2 are
interchangeable in all appropriate contexts if and
only if they have the same denotation. For most
programming languages, it's hard to come up with a
fully abstract denotational semantics because there
will usually be some theoretical possibility that the
mathematical machinery is capable of expressing but
the programming language isn't.
That means, rather counter-intuitively, that fixing
a failure of full abstraction usually involves making
the language more expressive, i.e. more able to tell
the difference between p1 and p2, i.e. more operational,
i.e. less abstract.
Although the more theoretically inclined semanticists
are often inclined to worry about failures of full
abstraction, those failures aren't such a big problem
when proving the correctness of compiler optimizations.
The bigger problem is that a denotational semantics is
seldom operational enough to express a transformation's
enabling conditions.
Mitch Wand and his students have made some impressive
progress on this problem, but it is my impression that
you still have to resort to operational semantics when
proving the correctness of most compiler optimizations.
* * *
References for Part 1
=====================
[1] Hanne Riis Nielson and Flemming Nielson.
Semantics with Applications: A Formal Introduction.
John Wiley, 1992.
[2] http://www.ccs.neu.edu/home/will/csu390-w07/turing1.sch
[3] J D Guttman, J D Ramsdell, and M Wand.
VLISP: A Verified Implementation of Scheme.
Lisp and Symbolic Computation, 8 (1995), pages 5-32.
More information about the PRL
mailing list