Goal
The purpose of this document is to introduce the denotational approaches to
programming language semantics. Two styles are presented: direct and
continuation. Direct is suitable for structured languages while continuation semantics
handle languages that can exit from inside structures. These notes introduce
the mathematical theory that demonstrates that denotational semantics defines
a well defined mathematical object for each part of program.
These notes discuss and develop the denotational semantics of While. While was
defined in
[ The Language While in while ]
The heart of this is the theory of the mathematical systems used in
denotational systems: Scott's theory of complete posets or domains
[ fixed.html ]
- DS::=following
- (Den1): maps each string in each syntactic category into a mathematical object.
- (Den2): is strictly compositional
- (Den3): is a set of equations
The definitions of the syntax must be echoed in the denotational semantics:
If the syntax defines construct X in terms of A B C then the denotational
semantics defines the meaning of X in using the meanings of an A, B, and C
only.
Previously we were able to define a semantic function in terms of the natural
semantics of the language, however we did not have such a compositional
definition for the function. But we have seen two examples of denotational
semantics already.
Integer Expressions
[ Semantics of Expressions in while ]
Boolean Expressions
[ Semantics of Boolean Expressions in while ]
The idea is to simplify the definition of a language by using more powerful
mathematical models. For example the definition of the semantic map A of an
Aexp is less complex than the semantics B of Bexp because each Aexp is
associated with an algebraic expression - an object in a known mathematical
system. The special cases in B used to define the meaning of Bexp would
not have been needed if tt and ff had been the elements in a classical
Boolean algebra with two elements. For example the four rules in Bexp that
define the boolean operators ~ and /\ are:
- part_of_Bexp::=following,
Net
- if B <<b >> s=tt then B <<~b >> s=ff,
- if B <<b >> s=ff then B <<~b >> s=tt,
- if B <<b1>> s=tt and B <<b2>> s=tt then B <<b1 /\ b2>> s=tt,
- if B <<b1>> s=ff or B <<b2>> s=ff then B <<b1 /\ b2>> s=ff.
(End of Net)
But if {tt, ff} was a Boolean algebra with negation - and conjunction '*'
then we would have to only write two rules, not four:
- alternative_to_Bexp::=
Net{
- BOOLEAN_ALGEBRA(V=>{tt,ff}, 0=>ff, 1=>tt).
- B <<~b >> s= - B <<b >> s.
- B <<b1 /\ b2>> s=B <<b1>> s * B <<b2>> s.
}=::alternative_to_Bexp.
Similarly the definition of Bexpp can be greatly simplified by (1)
assuming {tt,ff} is a Boolean algebra with negation, conjunction, disjunction
etc. Hint: why not use the same symbols in the Boolean algebra are is Bexpp
whenever possible?
The effect on the programmer is profound... the language means what it says!
Indeed expressions in the language can be treated as if they where really
elements in the same algebra. A set of denotational semantics almost
guarantees that the language is unlikely to surprise its users, A
mathematician would say, with good reason, that denotational semantics defines
a homomorphism between the syntax and the semantics. However compiler writers
would have a difficult problem - for example such a correspondence would
raise questions about whether short-circuit evaluation was permitted.
Another problem occurs when we define the ints as mathematical integers.
The finite representation
that is available and efficient can not be mapped into the normal
algebra of the integers. This means that a compromise would have to be
created where the semantics of ints is defined in terms of
a finite approximation to the integers. This is usually done informally.
The idea of using denotations that are elements in algebras could
formalize this idea precisely.
For a simple language like While it is enough for the
mathematical model to be a set of partial functions mapping the state of the
variables (itself a function) into another state. To make the model more
rigorous a pseudo-element undefined is added to the states:
- D <<S >> s is undefined iff `the statement S in state s does not
terminate`.
- D <<S >> s=s' iff the statement S in state s terminates in state s'.
The semantics will use three ways of combining functions:
- function::a set of partial maps a set to itself, assumed to be closed under the following operations.
- To see why we don't make this every partial function see
[ A Paradox ]
below
- Id::function=the identity mapping,
- For x, Id(x)=x.
- o::function><function->function.
- (composition): f o g = apply g and then apply f.
- cond::Boolean><function><function->function.
- (selection): cond(B, f, g)= fun[x](if B(x) is tt then f(x) else use g(x)).
- FIX::(function->function)->function.
- (Fixed Point): FIX F = a special function f such that F(f)=f.
If you think that function composition and such are not easy to program
then look at
[ fun.sml ]
The choice of the best of the available fixed points leads to the theory in
the heart of these notes.
[ Theory of Fixed Points ]
The following the expresses the Direct Denotational Semantics of
While:
- WHILE_DS::=
Net{
- State::=Var->Int.
- D::Stm->(State <>-> State).
- For S:Stm, s:State, D <<S >> s=the next state if and only if the statement S terminates in D <<s >> when started in state s.
- D <<x:=a >> = fun[s](s[x+>A <<a >> s]).
- D <<skip >> = Id.
- D <<S1;S2>> = D <<S2>> o D <<S1>> .
- D <<if b then S1 else S2>> = cond( B <<b >> , D <<S1>> , D <<S2>> ).
- D << while b do S >> = (FIX F) where F(g) = cond( B << b >> , g o D << S >> , Id)).
}=::WHILE_DS.
Each definition defines the meaning of a statement as an expression in the
mathematical calculus of relations and functions: Id, fun, o, cond, FIX.
The definition of D <<x:=a >> implies that if x=y then D <<x:=a >> s y = A <<a >> s
but if not x=y then D <<x:=a >> s y = s y. Similarly for all variables x,
D <<skip >> s x = s x.
The composition rule defines a unique successor state if and only if both
component are defined. Also note that the order of S1 and S2 are reversed on
opposite sides of the definition. Recall "f o g" = "g; f".
The semantics of if b then S1 else S2 uses a special function
cond( B <<b >> , S1, s2). Notice that it takes three functions and returns a
function:
- cond::(state->{tt,ff} >< (State<>->State) ><(State<>->State) -> State<>-
>State.
The defining properties of cond are
- if p(s)=tt then cond(p, g1,g2)s = g1(s),
- if p(s)=ff then cond(p, g1,g2)s = g2(s).
This means that as long as p(s) selects a function (g1,g2) that is defined on
s then the result is defined as well at s. Thus cond is a total function,
even if g1 and g2 are partial functions. In fact cond is always defined
even if some of its values cond(p,g1,g2)s are undefined!
I prefer to define f | g as behaving like f when f is defined and like g
when g is defined. However it is an error if f and g are both defined. An
alternative is f |-> g which behaves like f when f is defined and otherwise like g.
The definition of D <<while b do S >> is the cleverest part of these
semantics. The fixed point operator FIX and the functional F on which it
operates on a carefully chosen to give precisely the effect we want, without
using any form of explicit recursion.... the recursion is hidden inside FIX!
To show that this definition is going to work like previous ones, and to gain
understanding of how FIX and F work we can show that if we want this
- D <<while b do S >> = D <<if b then (S; while b do S) else skip >>
property to be true then we need to define D <<while b do S >> as shown. So
just suppose we didn't know the definition...
Let
- W:=while b do S,
- c:=B <<b >> ,
- d:=D <<S >> ,
- w:=D <<W >> ,
- Define F by For all g, F g = cond(c , g o d, id ).
- D << if b then (S; W) else skip >> = cond ( c, D <<S; W >> , D <<skip] )
- =cond ( c, D <<W >> o D <<S >> , Id )
- =cond ( c, w o D <<S >> , Id )
- =cond ( c, w o d, Id )
- = F (w )
But we want this to equal w so, we want F(w) = w.
(Close Let )
In other words to get the structural (operational) semantics of a while loop we need
to choose to define the denotation of a while loop to be a fixed point of the
specific functional chosen.
Note: We use the term functional for F to remind us that it is a function
that operates on other functions. The terminology is inherited from
functional analysis.
- W=while ~(x=0) do skip
Example 2
Let
- W:=while 0<=x do x:=x-1.
- |-(F g)s = cond(B <<0<=x >> , g o D <<x:=x-1>> , Id)s.
- |-If s x >= 0 then (F g)s = g o D <<x:=x-1>> s = g(s[ s x +> s x -1])
- |-If s x < 0 then (F g)s = Id s = s.
(Close Let )
Exercise 1
Let
- W:=while ~(x=1) do (y:=y*x; x:=x-1)
- Write down what (F g) s is.
- What are the functions g0, g1, g2, g3, defined by:
- g0 is undefined everywhere,
- g1 = F(g0),
- g2 = F(g1),
- g3 = F(g2),
- g4 = F(g3).
- What happens to the set of states for which g[i] is defined as
we apply this iterative process?
- Can you see a general pattern in the successive ges?
(Close Let )
[ Partial answer to Exercise 1 ]
Can we be sure that the definition of While actually defines a unique meaning
for D <<while b do S >> ? And why can we be sure? And what is the general rules
that make this sure.
Net
- (2a): Find F for W=while ~(x=0) do x:=x-1).
- (2b): Lists 5 functions f1..f5, which satisfy F(f)=f?
(End of Net)
Exercise 3
Net
- (3a): Write down the F for W=`while ~(x=1) do (y:=y*x; x:=x-1)
- (3b): (Harder) find a couple of f's for which F(f)=f.
- (Hint) (if you can't think of a fixed point, try iterating
- toward one...
- g0 is undefined everywhere
- g1 = F(g0)
- g2 = F(g1)
- g3 = F(g2)
- .... what is the pattern?
- For a second fixed point follow this hint.
- It will have the same values as the first one
- when the first one is defined. But it can
- have more defined values than the first one.
- )
(End of Net)
We will show that all the functionals of the following form
- F=fun[g]cond( B << b >> , g o D << S >> , Id)
do have fixed points. We will also choose the particular fixed point of F
that gives us the precise properties need to make this semantics work the way
we our experience and intuition suggest. Very roughly we are looking for a
fixed point that stops the loop as soon as possible. Or put it another way, we
know that computers tend to produce infinite loops whenever. We therefore
want the meaning of a loop to be as undefined as possible, and yet to still
reflect the iteration. We want the fixed point that tells us the least about
what is going to happen. -- this is a bit fuzzy, a formal version follows.
Now suppose that s'=D <<S >> s and B <<b >> s = tt and that g is such that F(g)=g,
then
- |-g(s) = g(s').
In other words, a fixed point function has a constant value when applied to
success iteration round a while loop. Because
- |-g(s) = F(g)(s)
- = cond( B << b >> , g o D << S >> , Id)(s)
- = (g o D << S >> )s
- = g( D << S >> s)
- = g(s').
Similarly you can show that if D <<S >> s is undefined and
B <<b >> s=tt and F(g) = g, then g(s) is undefined.
Also we have (please work out why) that whatever D <<S >> is, if
B <<b >> =ff implies that (F g)s = s.
Prove the last two results - the proofs are like the first one above.
Consider three case:
When the loop W=while b do S terminates for a given initial state.
- Here any fixed point of F has the expected effect on the state.
When the statement the loop (S) fails to terminate and loops after being
repeated (and terminating) a number of times.
- Again any fixed point of F will generate the right sequence of states
- and then be undefined.
When the W loop itself loops from a given initial state of s0, even tho' S
terminates each time.
- This means that we have a sequence of states s1,s2,s...,s[i],... and
- for all i, B <<b >> s[i] = tt and D <<S >> s[i]=s[i+1].
So, for every step of the way a fixed point g of F will remain
the same
- g(s[0]) = g(s[i]).
TBA
This shows that if a function F has a fixed point FIX F then it can be
found by iterating F in a Kleene sequence: {}, F{}, F F{}, F F F{}, which
should fit with our intuitive feel for the meaning of loops.