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 ]

Denotational semantics

1. DS::=following

   ---

   1. (Den1): maps each string in each syntactic category into a mathematical object.
   2. (Den2): is strictly compositional
   3. (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.

   Examples

   Integer Expressions [ Semantics of Expressions in while ] Boolean Expressions [ Semantics of Boolean Expressions in while ]

   Idea

   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:
2. part_of_Bexp::=following,
   Net
   1. if B <<b >> s=tt then B <<~b >> s=ff,
   2. if B <<b >> s=ff then B <<~b >> s=tt,
   3. if B <<b1>> s=tt and B <<b2>> s=tt then B <<b1 /\ b2>> s=tt,
   4. 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:
3. alternative_to_Bexp::=
   Net{

   1. BOOLEAN_ALGEBRA(V=>{tt,ff}, 0=>ff, 1=>tt).
   2. B <<~b >> s= - B <<b >> s.
   3. 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.

   Basis of Denotational Semantics

   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:
4. D <<S >> s is undefined iff `the statement S in state s does not terminate`.

5. D <<S >> s=s' iff the statement S in state s terminates in state s'.

   The semantics will use three ways of combining functions:

   Operations on Functions

   ---

   1. function::a set of partial maps a set to itself, assumed to be closed under the following operations.
   2. To see why we don't make this every partial function see [ A Paradox ] below
   3. Id::function=the identity mapping,
   4. For x, Id(x)=x.

   5. o::function><function->function.
   6. (composition): f o g = apply g and then apply f.

   7. cond::Boolean><function><function->function.
   8. (selection): cond(B, f, g)= fun[x](if B(x) is tt then f(x) else use g(x)).

   9. FIX::(function->function)->function.
   10. (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 ]

. . . . . . . . . ( end of section Introduction) <<Contents | Index>>

Semantics of While

The following the expresses the Direct Denotational Semantics of While:
1. WHILE_DS::=
   Net{

   1. State::=Var->Int.
   2. D::Stm->(State <>-> State).
   3. 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.
   4. D <<x:=a >> = fun[s](s[x+>A <<a >> s]).
   5. D <<skip >> = Id.
   6. D <<S1;S2>> = D <<S2>> o D <<S1>> .
   7. D <<if b then S1 else S2>> = cond( B <<b >> , D <<S1>> , D <<S2>> ).
   8. D << while b do S >> = (FIX F) where F(g) = cond( B << b >> , g o D << S >> , Id)).
   
   }=::WHILE_DS.

   Explanations

   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:

2. cond::(state->{tt,ff} >< (State<>->State) ><(State<>->State) -> State<>- >State.

   The defining properties of cond are

   ---

   1. if p(s)=tt then cond(p, g1,g2)s = g1(s),
   2. 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!

   Note: How I do Cond

   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.

   Definition of the loop semantics

   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
3. 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

   1. W:=while b do S,
   2. c:=B <<b >> ,
   3. d:=D <<S >> ,
   4. w:=D <<W >> ,
   5. Define F by For all g, F g = cond(c , g o d, id ).

   6. D << if b then (S; W) else skip >> = cond ( c, D <<S; W >> , D <<skip] )
   7. =cond ( c, D <<W >> o D <<S >> , Id )
   8. =cond ( c, w o D <<S >> , Id )
   9. =cond ( c, w o d, Id )
   10. = 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.

   Example 1

4. W=while ~(x=0) do skip

   Example 2

   
   Let
   1. W:=while 0<=x do x:=x-1.

      
      

   2. |-(F g)s = cond(B <<0<=x >> , g o D <<x:=x-1>> , Id)s.
      
   3. |-If s x >= 0 then (F g)s = g o D <<x:=x-1>> s = g(s[ s x +> s x -1])
      
   4. |-If s x < 0 then (F g)s = Id s = s.
   
   (Close Let )
   

   Exercise 1

   
   Let
   1. W:=while ~(x=1) do (y:=y*x; x:=x-1)
   2. Write down what (F g) s is.

   3. What are the functions g0, g1, g2, g3, defined by:

      ---

      1. g0 is undefined everywhere,
      2. g1 = F(g0),
      3. g2 = F(g1),
      4. g3 = F(g2),
      5. g4 = F(g3).

      ---

   4. What happens to the set of states for which g[i] is defined as we apply this iterative process?
   5. 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.

   Exercise 2

   
   Net
   1. (2a): Find F for W=while ~(x=0) do x:=x-1).
   2. (2b): Lists 5 functions f1..f5, which satisfy F(f)=f?
   
   (End of Net)
   

   Exercise 3

   
   Net
   1. (3a): Write down the F for W=`while ~(x=1) do (y:=y*x; x:=x-1)
   2. (3b): (Harder) find a couple of f's for which F(f)=f.
   3. (Hint) (if you can't think of a fixed point, try iterating
   4. toward one...
   5. g0 is undefined everywhere
   6. g1 = F(g0)
   7. g2 = F(g1)
   8. g3 = F(g2)
   9. .... what is the pattern?
   10. For a second fixed point follow this hint.
   11. It will have the same values as the first one
   12. when the first one is defined. But it can
   13. have more defined values than the first one.
   14. )
   
   (End of Net)
   

   We will show that all the functionals of the following form

5. 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
   

6. |-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
   

7. |-g(s) = F(g)(s)
8. = cond( B << b >> , g o D << S >> , Id)(s)
9. = (g o D << S >> )s
10. = g( D << S >> s)
11. = 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.

    Exercise 3

    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.
    1. 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.

    2. Again any fixed point of F will generate the right sequence of states
    3. and then be undefined.

       When the W loop itself loops from a given initial state of s0, even tho' S terminates each time.

    4. This means that we have a sequence of states s1,s2,s...,s[i],... and
    5. 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
12. g(s[0]) = g(s[i]).

    TBA

. . . . . . . . . ( end of section Semantics of While) <<Contents | Index>>

Theory of Fixed Points

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.

Existence of Direct Semantics for While

Semantic Equivalence