Programming Languages Semantics with Applications / Prof

Programming Languages Semantics with Applications / Prof. Mooly Sagiv
Lecture #3, 18/5/08: Denotational Semantics

Notes by: Tom Yam and Michael Kuperstein

Denotational semantics

So far, we have investigated operational semantics.In which, the equivalence of commands is defined as c1~c2,' (<c1,)' (c2,)'). When we wished to proof equivalence of commands, for example

B1~B2 while B1do com ~ while B2do com

we had to use the rules and axioms.

Denotational semantics defines the semantics of commands, arithmetic and Boolean expressions as mathematical entities mapping input to output, ignoring the intermediate states. Inaccurately, we can describe the semantics of a command as s function  (from the states space to the states space).

The semantics of a command or expression will be denoted using square brackets C

For example, the semantics space for IMP will be as following:

A: Aexp  (N)

B: Bexp  (T)

C: Com  ()

The term "function" is inaccurate to describe the semantics of a command. The term "partial function" is more suited.This means that for some states, the command might not be defined. We need this change to overcome commands such as 'if (x=0) while true do skip; else x:=x+1' which are not well defined for all states (in that specific example, for any state for which x is 0).

Denotational semantics of IMP

We will now define the denotational semantics of the IMP language, using structural induction.

Denotational semantics of Aexp

A n / = {(, n) | }
A X / = {(, (X)) | }
A a0+a1 / = {(, n0+n1) | (, n0)Aa0, (,n1)Aa1}
A a0-a1 / = {(, n0-n1) | (, n0)Aa0, (,n1)Aa1}
A a0a1 / = {(, n0 n1) | (, n0)Aa0, (,n1)Aa1}

We can also use the Lambda notion to describe the Denotational semantics of Aexp

A n / = .n
A X / = .(X)
A a0+a1 / = .(Aa0+Aa1)
A a0-a1 / = .(Aa0-Aa1)
A a0a1 / = .(Aa0 Aa1)

For example the semantic of A7 - 3 is

A7 - 3 / = (1st rule)
= .(A7 - A3) / = (4th rule)
= .((.7) - (.3)) / = (simple calculus)
=.5+3 / = (computation)
= .8

Denotational semantics of Bexp

B true / = {(, true) | }
B false / = {(, false) | }
Ba0=a1 / = {(,true) |  & Aa0=Aa1}
{(, false) |  & Aa0Aa1}
Ba0a1 / = {(, true) |  & Aa0 Aa1}
{(, false) |  & Aa0Aa1}
B b / = {(, Tt) | , (, t) Bb}
B b0b1 / = {(, t0Tt1) | , (, t0) Bb0, (, t1) Bb1 }
B b0b1 / = {(, t0Tt1) | , (, t0) Bb0, (, t1) Bb1 }

We can also use the Lambda notion to describe the Denotational semantics of Bexp

B true / = .true
B false / = .false
Ba0=a1 / = .true if Aa0=Aa1 else false
Ba0a1 / = .true if Aa0Aa1 else false
B b / = .Bb
B b0b1 / = . Bb0 Bb1
B b0b1 / = . Bb0 Bb1

Lemma 3.1 (denotational semantics is well-defined): Both Aa and Bb are functions for any arithmetic expression a or Boolean expression b.

Proof: by structural induction.For Aexp, we need to show for every state  that there exists exactly one pair (,n).

Base:For expressions of the form 'n' and 'X', it is obvious.

Hypothesis: Assume it's correct for expressions of nesting level i.

The Move: Let A be an expression with nesting level i+1.

A can be a0+a1, a0-a1 or a0a1.

Let A=a0+a1and . Aa0+a1={(, n0+n1) | (, n0)Aa0, (,n1)Aa1}. From the induction assumption there exists exactly two (,n0)Aa0, (,)Aa0. Therefore (, n0+n1) is well defined and is single.The proof of the rest of the cases is similar.

The proof for Bexp is similar.



Denotational semantics of commands

Our aim is to represent commands as functions. Commands start on a state  and yield another state ’. A Command is just a “state-mutator”.

We don't wish to limit ourselves to particular commands; neither do we know how to do so syntactically. Without loops, commands will always terminate, but we can't do much without loops.

To deal with undefined states and commandswhichdon't end, we introduce the element  to denote the outcome whichstands for non-termination. This spares us the need to deal with partial functions.

For any set X, Xdenotes X  {}.

We can now extend commands from partial functions  complete functions  by mapping any  in the input to. This behavior is normal because if a part of a program doesn't terminate, the entire program won't terminate.

Cskip / = {(,)|} (the identity function)
C X:=a / = {(, [n/X]) |  & n=Aa}
C c0;c1 / = C c1C c0
C if b then c0 else c1 / = {(, ’) | Bb=true & (, ’) Cc0}
{(, ’) | Bb=false & (, ’) Cc1}
Cwhile b do c / = ???

What can we do for the while command? We want "while B do C" to be equivalent to "if B then (C; while B do C) else skip". We wish the equivalence to be mathematical, i.e. the while loop will be a function  satisfying the equation. Is there a solution to the equation? Is it unique?

Let W denote "while B do C". From the equivalence, we derive the recursive equation

W() = if Bb then W(Cc) else 

We now need to find a solution to this equation.

Domain Theory

Let's think of a program as a processor of stream (finite or infinite) of bits ({0, 1}). For example, lets "isone" be a program receiving a stream of bits, with a terminating $, as input. It returns 1$ if there is at least one"1" in the input and 0$ otherwise.

If all we've encountered so far are 0's, we can't return yet. The correct return might be 1$ or 0$ so we must return a prefix of them, which is only . Other return values might make the program retracts its answer.

Definition 3.2 (partial order):A partial order (po) is a set P on which there is a binary relation  which is:

Reflexive: pP. p  p
Transitive: p,q,r  P. p  q & q  r  p  r
Antisymmetric: p,q  P. p  q & q  p  p = q

Thinking about x and y as inputs to this program we get an intuitive definition of the partial order:

Intuitive definition 3.3 (partial order): Example partial order x yinclude:

x is a prefix of y.

y is a refinement of x

The notion that the programnever retracts its answer is the intuitive definition of the monotonicity property

Definition 3.4 (poset): A set equipped with a partial order is called a poset.

Definition 3.5 (monotonic function):Let D and E be posets. A function f: D E is monotonic if: x,yD: x D y  f(x) E f(y).

The semantics of a program ought to be a monotonic function in the sense that more information about the input leads to more information about the output

Claim 3.6 (isone(0k)=): Consider our “isone” function with the prefix ordering. Lets denote 0kas the stream of k consecutive 0’s and 0 is the infinite stream of 0’s.

We will now formally prove that isone(0k ) = 

Proof:

By definition, isone(0k$) = 0$ and isone(0k1$) = 1$.

But 0k0k$ and 0k 0k1$and from the monotonicity of “isone” we get:

•isone( 0k )  isone( 0k$) = 0$

•isone( 0k )  isone( 0k1$) = 1$

Therefore, monotonicity requires that isone(0k ) is a common prefix of 0$ and 1$, namely .



Let's try to define isone recursively. One might write isone as:

isone()=
isone(1s)=1$
isone(0s)=isone(s)
isone($)=0$

This definition is not well-defined for infinite streams. We need infinitestreams when we deal with non-terminating programs. Continuity means finite output depends only on finite input. There might be an infinite output, but infinite behavior must be the limes of the finite behavior.

Definition 3.7 (chain): A chain is a countable increasing sequence

<Xi> = { xi X | x0  x1  … }.

Definition 3.8 (upper bound): Let P be a poset (P, ), and X be a subset of P. pP is an upper bound of X if:qX. q  p

Definition 3.9 (least upper bound): p is the least upper bound (lub) of X if:

p is an upper bound of X, and
for all upper bounds q of X, p q

Note that, if exist, the lub is unique, this follows from the Antisymmetric property of the po (xy and yx  x=y).

Example 3.10 (a poset with no upper bound): Look at the set N with the following po:  n and n  n  nN.This is indeed a poset. It's reflexive and it's transitive and Antisymmetric holds in the empty aspect. There is no upper bound to this poset because the elements in N are not comparable to each other (they are only bigger than bottom).

Example 3.11 (another poset with no upper bound): The set {1, 2} does not have an upper bound, with respect to the po 11 and 22.

Example 3.11 (yet Another poset with no upper bound): Look at the set of all natural numbers with the po (0  1  2  …). Although the elements are comparable to one another, there is no upper bound. Note that this poset is also a chain.

Example 3.12 (posets with upper bound):The sets {1}, {1,} and {2,} all have upper bunds with respect to the po from exaple 3.10. The upper bounds are 1, 1 and 2 respectively.

It is convenient to work with posets where every chain (not necessarily every set) has a least upper bound

Definition 3.13 (complete partial order):A partial order P is a complete partial order (cpo) if every chain in P has a least upper bound also in P.

Definition 3.14 (pointed cpo):A cpo with a least (“bottom”) element  is a pointed cpo (pcpo).

Example 3.15 (a flat cpo): Any set P with the po x  y  x = y is a cpo. Every chain in P has only one element, which may appear many times. This elements is also the upper bound and the least upper bound.Such cpos are called flator discretecpos.

Example 3.16 (a flat pcpo): The poset from example 3.10 is a flat pcpo. All chains have one or two elements (a number nN and without  or just one xN).In the case that appears, it is also the least upper bound. In all other cases the additional nN is the least upper bound.

Example 3.17 (not a cpo): The poset with bottom from example 3.11 is not a cpo because the chain 012… has no least upper bound in N.

Example 3.18 (a pcpo): The set N  {  } with (012…) is a pointed cpo. For every finite chain the last element is the least upper bound of the chain and in the infinite case  is the least upper bound.

Example 3.19 (not a pcpo): The set N with  is a cpo without bottom, not a pcpo. For every finite chain the least upper bound is the last element. If the chain is infinite there is not "last" element.

Lemma 3.20 (cpo construction)

Given two pcpos D and E, is also a pcpo with the partial order defined as if and only if and .

The constructed pcpo has the following properties:

2. For two chains <xi>, <yi>, the least upper bound of <(xi, yi)> is (xi, yi,)

If D and E are posets and f: D E is a monotonic function, it follows from definition 3.5 that applying f to a chain of inputs produces a chain of outputs

Under the above conditions, the following holds:

Claim 3.21

Proof

Because is an upper bound,

f is monotonic, hence applying it to both sides we get

That means is an upper bound on, and since is the least upper bound, .

The converse of claim 3.19 is not true. That is, it is not always the case that.

Example 3.22

The poset with the relation includes the chain of all natural numbers (without) 0  1  2  … Let us define the function f as illustrated below:

, .

f is obviously monotonic.
However, and, so .

The previous example shows that, intuitively, the condition does not hold because of a discontinuity in f: there was a "jump" in the value of f when moving from finite to infinite input. This is exactly the intuition we would like to capture in the next definition:

Definition 3.23

Given posets D and E and a function f: D E, f is called continuous if for any chain , it is true that.

If f is monotonic, then due to claim 3.19, f is continuous if and only if.

If we go back to the semantic interpretation of f, it can be said that each f(xi) uses a "finite" view of the input, while f() uses an "infinite" view. The continuity condition means that the output generated using an infinite view of the input does not contain more information then all of the outputs based on finite inputs.

Example 3.24

For the partial order {,} the identity function id(n) = n is continuous:, , so

Example 3.25

For the same partial order the constant function five(n) = 5 is continuous: , , so .

Example 3.26

For any flat cpo A, any monotonic function such that is continuous. trivially holds for finite chains.is a flat pcpo, so all infinite chains are of the form or
In both cases, .

Going back to the semantics of the while command, our goal was to find a function W: that satisfies the intuitive semantics of "while b do c".

Thus, we need to solve the following recursive equation:

where

We can turn this into a fixed point equation by defining the function F as

and then solving W=F(W), that is finding a fixed point of F.

Typically, F will have many fixed points.However, since we want our semantics (and, specifically, the function W) to be continuous, we can significantly cut the number of solutions. We will see how to find the least fixed point of F, provided that F itself is continuous.

Theorem 3.27 (Fixed Point Theorem)

Define (F composed k times).

Then:

For any fixed point x of F and any, .
The least of all fixed points of F is.

Proof:

By definition, . Through repeated application of F to both sides of the equation and due to monotonicity, we get that is a chain.

Then, the proof of (1) is by induction:
Base: by definition,

Induction step: Suppose. F is monotonic, so and because F(x) = x, .

To prove (2), we need to show is a fixed point, and it is less than or equal to any other fixed point. Because F is continuous,and because , we get that is indeed a fixed point.
From (1), for any other fixed point x, for any k,.Therefore x is an upper bound on the chainand since is the least upper bound,

Since the theorem is constructive, if F is continuous on a pointed cpo, we know how to find the least fixed point. All other fixed points can be considered refinements of the least one and contain more information. However, they are also more arbitrary and make less sense for the purpose of defining W.

Denotational Semantics of IMP – Part 2

, the set of all configurations, is a flat pointed cpo. Any configuration has more information than non-termination, so for any , . Otherwise, the states must be equal to be comparable. We also define a partial order on the set of strict (and therefore continuous) functions in:

For if and only if . This means that whenever f terminates, g terminates with the same output state. On inputs on which f does not terminate, g may or may not terminate. Thus, g is a refinement of f for a larger set of inputs.

Recall that is a fixed point of

Since is continuous, so is F, and from the fixed point theorem we can set .
This is the least fixed point of F, meaning that it terminates least often of all fixed points, but when it does terminate, it agrees on the output state with all other fixed points.

It can be shown that the semantics we've defined is equivalent to natural semantics in the sense that . The full proof of that statement can be found in chapter 4.4 (pp. 112 – 116) of "Semantics with Application" (Nielsen & Nielsen).

Example 3.28

. Since this is an infinite loop, the expected result is.
Because, .

By definition. .

and it's easy to see that for any k, .

Thus, the least fixed point is , which is exactly what we expected.

Example 3.29

. If we restrict ourselves to, we expect that.

Again, in the context of semantic functions, so:

By induction, it can be shown that

And from that we get

Another way to find the least fixed point of F is by using complete partial orders.

Definition 3.30

Let be a partial order. D is a complete lattice if every subset has both a greatest lower bound and a least upper bound.

Note that the requirement is for every subset, not just every chain.

Theorem 3.31 (Knaster-Tarski Theorem)

Let be a monotonic function on a complete lattice L. The least fixed point of f exists, and is (where is the greatest lower bound).

Unfortunately, although the assumption is a complete lattice is reasonable this theorem does not provide a constructive method for finding the least fixed point.

To summarize, denotational definitions are not necessarily better than operational ones, and they require (like in the case of the while statement) more mathematical work. However, because they are compositional, they make some proofs easier than operational definitions. Denotational semantics can also be extended to support a wide variety of constructs, like expression with side-effects, loops, recursion, goto (although that is particularily hard), and non-determinism - but not low level concurrency.