[PRL] den sem
William D Clinger
will at ccs.neu.edu
Fri Mar 2 14:37:42 EST 2007
A Brief Introduction to Denotational and Operational Semantics
(Extended Abstract)
by William D Clinger
Part 2
NU PRL, 2 March 2007
I appreciate the interest you have shown by returning
for the second part of my talk. We'll start with a
quick review of my abstract and outline from yesterday:
Abstract:
Regarding denotational and operational semantics:
1. Both can be formal.
2. Both can be executable.
3. Neither has to be executable.
Outline:
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
* * *
Matthias's Example
==================
Yesterday I told you that, for sufficiently powerful
programming languages, we can't hope to define an
executable semantics that tells us which programs
won't terminate on which inputs. If we insist upon
a semantics that tells us such things, then the
semantics will not be executable.
That goes for both denotational and operational semantics.
Matthias graciously provided the following example
when he invited me to talk about this stuff. I quote
verbatim:
> Consider the simplistic programming language NEXEC
>
> An expression is one of:
> F(NE)
>
> An NE is one of:
> -- Zero
> -- Add1(NE)
>
> Here is the Scott model for NEXEC:
> <N_bot, f>
> where
> f : N_bot -> N_bot
> f(bot) = bot
> f(i) = 1 if Turing Machine i halts if i is on the tape
> f(i) = 0 if Turing Machine i diverges if i is on the tape
>
> The model consists of a Scott domain and a Scott continuous function
> from the domain to itself.
>
> Here is the denotational semantics:
>
> FF[F(NE)] = f(F[NE])
> F[Zero] = 0
> F[Add1(n)] = F[n] + 1
>
> I believe that this denotational semantics is not executable. If I am
> wrong, I'd be happy to be convinced otherwise.
Translating this into a notation with which I am more
comfortable, and changing the syntax slightly to make
it less confusing, the language is
NEXEC ::= Halts(NE)
NE ::= Zero | Add1(NE)
The semantics of the sublanguage NE is defined by a
compositional denotational semantics very much like
our denotational semantics for CONJUNCTION. The
semantics of the entire language NEXEC is also
compositional, but uses an auxiliary function f that
is clearly not computable. Hence the semantics as a
whole is not executable. (Matthias was neither the
first nor the most creative researcher to employ this
technique [4].)
The auxiliary function f is described in a way that
might create the false impression f has something to
do with Scott models, or has something to do with
nontermination of NEXEC programs or with \bottom, or
maybe with fixed point semantics. In truth, f has
nothing to do with any of that. Simplifying the
presentation of f to eliminate irrelevant clutter,
we see that f: N -> N is the total function defined by
f(i) = 1 if Turing Machine i halts if i is on the tape
f(i) = 0 if Turing Machine i diverges if i is on the tape
We can give an equivalent big-step operational semantics
as follows.
Zero --> 0
n --> j
k = j + 1
-------------
Add1(n) --> k
n --> j
k = f(j)
--------------
Halts(n) --> k
That gives us an example of an operational semantics
that is not executable, which (together with Matthias's
example) establishes the third claim of my abstract.
Before we leave this language, let us consider what
an executable semantics for it would be like. We'll
have to give up on having the semantics tell us which
programs won't terminate on which inputs, but it
will be able to tell us which programs do terminate
on which inputs.
This time we'll do the big-step operational semantics
first, because I don't intend to bore you with all its
details. Interested parties are encouraged to examine
the actual Scheme code [5,6].
Zero --> 0
n --> j
k = j + 1
-------------
Add1(n) --> k
n --> j
(halts? j j)
--------------
Halts(n) --> 1
The above big-step operational semantics for NEXEC is
executable in exactly the same sense that all three of
the Nielsons' semantics for WHILE are executable [7].
We will now define an executable denotational semantics
for NEXEC. It is not compositional, because we want our
executable semantics to be compatible with Matthias's,
and Matthias's use of Goedel numbering is more like an
encryption of a Turing machine than a description. Our
semantics will, however, be the composition of two
compositional denotational semantics, separated by a
decryption step:
FF[Halts(n)] = g(machine(F[n]))(tape(F[n]))
F[Zero] = 0
F[Add1(n)] = F[n] + 1
where machine: N -> TURING is my Goedel un-numberer [8],
tape: N -> X* translates natural numbers to unary for
the input tape, and g: TURING -> (N ->_\bottom {true})
assigns a denotation to each Turing machine. Those
denotations are partial functions from inputs to a
domain whose one proper value indicates that the machine
halts. The domain does not even contain any values that
could be used to indicate the machine does not halt.
The TURING language matches the representation
generated by my Goedel un-numberer, and is a proper
sublanguage of the representation expected by my Turing
machine interpreter:
TURING --> () | (B A)
A --> \epsilon | B A
B --> (Q (X X D Q) (X X D Q))
X --> _ | 1
D --> L | R
where L and R are the Scheme symbols L and R, and Q is
a Scheme symbol naming a state.
The semantic domains and functions are
Config = X* Q X*
Cont = Config -> Config
Env = Q -> Cont
g: TURING -> (X* ->_\bottom {true})
t: TURING -> Cont
a: A -> (Env -> Env)
b: B -> (Env -> Env)
In the interest of shortening this presentation and
saving myself some preparation time, I will define
only the first two semantic functions:
g(())(n) = true
g(((q (_ x0 d0 q0) (1 x1 d1 q1)) ...))
= t(((q (_ x0 d0 q0) (1 x1 d1 q1)) A))
(make-config n q \epsilon)
t(())(c) = c
t(((q (_ x0 d0 q0) (1 x1 d1 q1)) ...))(c)
= let r = fix (lambda r .
a(((q (_ x0 d0 q0) (1 x1 d1 q1)) ...))(r))
in r(q)(c)
Those definitions are untested. Completion of the
executable denotational semantics for TURING is left
as an exercise for the reader. For full credit, your
semantics will be written in a purely functional
subset of portable Scheme and will be fully equivalent
to the executable big-step semantics defined above.
Nondeterminism
==============
In 1976, when Michael Rabin and Dana Scott were both
given ACM's A. M. Turing Award, the official citation
referred to their joint paper that introduced the
concept of nondeterministic automata. The citation
did not mention Scott's work on semantics [8].
Among PL researchers, Scott is better known for his
work on domain theory, which was motivated in part by
his desire to find a nontrivial model for pure lambda
calculus. (The obvious semantic domain for the lambda
calculus is D = D -> D. If you interpret D -> D as
the set of all functions from D to D, then there is
exactly one solution to that domain equation, and
that solution contains exactly one function, which
maps itself to itself. The people who were using
lambda calculus as a metalanguage to develop formal
descriptions of programming languages didn't like
the idea that every lambda term means exactly the
same thing as every other lambda term.)
Because Scott's work was devoted to finding nontrivial
models for the lambda calculus, his results mostly
had to do with functions, which are the epitome of
determinism. To deal with nondeterminism, Scott's
results have been extended to relations and to
power domains (which are basically set-valued
functions), but neither of these extensions has
proved to be entirely satisfactory. With power
domain semantics (which I understand better than
relational semantics), the main problem is that
it is hard to come up with a partial order that
doesn't conflate possible results x and y with
operationally impossible or undesired results that
lie between x and y in the ordering.
As this is essentially a topological problem, the
denotational semantics of a nondeterministic language
often uses some topology other than Scott's. This
trend away from Scott topologies has made denotational
semantics less accessible to computer scientists.
Big-step and small-step operational semantics, on
the other hand, are nondeterministic by nature; when
working with such semantics, determinism should never
be assumed without proof. Familiarity, simplicity,
and nondeterminism have all contributed to the trend
toward operational semantics instead of denotational.
Denotational and Operational Semantics of First Order Logic
===========================================================
Denotational semantics is older than Dana Scott.
Development of the most important denotational
semantics began in the early 1930s.
Alfred Tarski's truth-theoretic semantics for first
order logic is denotational. All of the later work
on denotational semantics and model theory, including
Kripke's for modal logic, Cohen's for set theory,
and Scott's for programming languages, builds on
Tarski's pioneering semantics.
First order logic also provides the canonical
example of a relationship between a non-executable
denotational semantics and an executable operational
semantics.
Non-executable Semantics for First Order Logic
==============================================
Tarski's semantics for first order logic goes
roughly like this: you start with a universe U
(which is like the underlying set of a domain);
then you add an interpretation I, which assigns
meanings to constants, function symbols, and
predicates; then, using environments to map
variables to elements of U, you define the
semantics of all formulas. In essence, the
denotation of a formula is a function from
universes, interpretations, and environments
to truth values.
The semantics is denotational, and is almost
compositional. For example, the meaning of
P & Q is defined in terms of the meanings of
P and Q like this:
I, rho |= P
I, rho |= Q
---------------
I, rho |= P & Q
The meaning of a universally quantified formula
is determined by this rule:
if, for every a in U:
I, rho[x=a] |= P
--------------------
I, rho |= forall x P
That is not executable.
Executable Semantics for First Order Logic
==========================================
Proof systems provide operational semantics for first
order logic. Suppose, for example, that A, ... |- P
means that you can prove P from assumptions A, ....
Then we have the rule
x does not occur free in A, ...
A, ... |- P
--------------------
A, ... |- forall x P
There are many beautiful connections between the
non-executable denotational semantics of first order
logic and its executable operational semantics, but
the two main results are:
Soundness. If |- P, then |= P.
Completeness. If |= P, then |- P.
One way to prove the completeness theorem for first order
logic involves showing how the non-executable denotational
semantics can be converted into an executable and
complete refutation procedure for the Herbrand universe
of ground terms.
Clarification of Matthias's Points
==================================
When he invited me to talk to you about these subjects,
Matthias suggested I comment upon the following points.
I quote verbatim.
> In general I believe that Scott's program really got at the following:
>
> 1. Scott domain constraints eliminate some "computational junk" but
> not all from semantic constraints.
I'm not sure what Matthias is getting at here, but it
isn't very important.
> 2. To get an executable model, you need to work within a Universal
> Domain, which can embed all domains from your category of domains of
> meaning, and with a Universal Programming Language.
That is untrue. As Mitch pointed out, executability is
the consequence of using only constructive mathematics
to define your semantics. In the area of nondeterministic
languages, for example, much excellent work has been done
using constructive metric spaces as domains, together with
the Banach fixed point theorem.
> 3. Once you have chosen a Universal Domain/Language, you prove once
> and for all that each domain and each program in the language are
> executable.
>
> For Scott, this meant in the early papers Pomega plus LAMBDA (!=
> lambda calculus), a language of combinators that directly denote
> elements from Pomega.
I agree that these general theorems ensuring executability
are one of the main arguments for working with a universal
domain and a standard metalanguage.
> As far as I know,
>
> (A) few people have done this work for other variants
> (B) few people write in Lambda these days.
(B) is true. Thanks to greater awareness of Church's thesis
and computability in general, authors no longer have to
waste page count on proving their metalanguage is executable,
so there is no reason to restrict yourself to a standard
metalanguage on that account.
As for (A), it depends on how you define "few". I would
say that many mathematicians have contributed to our current
knowledge of constructive mathematics, and everyone who does
research in denotational semantics relies on that knowlege.
> People (like Mitch) who did "compiler generation/correctness from Den
> Sem" tended to stay close to (2) and (3) above but I have also
> encountered people who built their own categories without Universal
> Language and without (3) and no guarantees about executability.
Mitch has already clarified what he does, and my approach
in that area has always been similar to Mitch's. As noted
above, (2) is incorrect. I agree with you about the last
bit; indeed, I recall one person in particular [4].
Responding to Mitch, Matthias wrote:
> > Umm, if I recall the correspondence correctly, I believe that what
> > Will claimed was that a denotational semantics could either be
> > executable or not executable. So your example merely confirms that
> > position.
>
> Perhaps I am really old, but you reversed the positions. I (wanted
> to) say that denotational specs don't have to be executable and Will
> made fun of my statement.
Mitch recalled the correspondence correctly, and stated my
position correctly. As for making fun of your statement,
I was pretty sure you hadn't meant what you actually said,
so I didn't take your statement very seriously, and used
jocular language to suggest you might want to clarify your
position. You did so by writing:
> Denotational semantics isn't executable. An operational semantics
> approximating the enumeration behavior of denotational semantics is.
I am glad we have both had this opportunity to clarify our
respective positions further.
Conclusions
===========
Both denotational and operational semantics can be formal.
Both can be executable. Neither has to be executable.
* * *
[4] Citations withheld to protect the guilty.
[5] http://www.ccs.neu.edu/home/will/csu390-w07/halts.sch
[6] http://www.ccs.neu.edu/home/will/csu390-w07/turing.sch
[7] Hanne Riis Nielson and Flemming Nielson.
Semantics with Applications: A Formal Introduction.
John Wiley, 1992.
[8] http://awards.acm.org/
* * *
Errata: In the list of references for yesterday's talk,
reference [2] should have given the URL given above for
reference [6].
More information about the PRL
mailing list