DENOTATIONAL SEMANTICS

OPERATIONAL SEMANTICS -- Where we have statements and logical derivations to prove that a program works, from basic principles.

DENOTATIONAL SEMANTICS -- translates a program into a function that "maps" memory states to memory states.

The distinction between the two is subtle.  Might be a distinction without a difference.

The book says that operational semantics are like an interpreter.  After using operational semantics you end up with a final state after applying the various inference rules.

Denotational semantics are more like a compiler.  A program is translated into a function that takes states to states, and so it's like one form is translated into the other.

However, at the end of day, in either semantics, you have a starting state and you end up with an ending state.  AND, you can prove that the two semantics are of equal power, which essentially says that they say the same thing and give the same information, just in a different format.

The biggest difference is that in denotational semantics, the infinite loop is explicitly part of the syntax.  In operational semantics, it is not.  In denotational semantics we have a symbol, the "uptack" or "upside-down T" to represent an unreachable memory state, aka an infinite loop.

Remember what a memory state is:  a function that maps variables to explicit integers.

Under denotational semantics, a program can be thought of as a function from SIGMA (the set of all possible memory states) to SIGMAT (the set of all possible memory states PLUS the infinite loop situation).

Now, to understand the book's syntax, we have to understand lifting, which is noted by a *.

if f is a function from SIGMA to SIGMAT, then f* is a function from SIGMAT to SIGMAT such f* (T) = T, and f*(sigma) = f(sigma) for everything else.  f* is exactly the same as f, except f* (infinite loop) is also an infinite loop.  This is because since an infinite loop isn't really a memory state, it falls out of scope for a function designed to map memory states to memory states, but this allows to define things like compound statements and while loops without having explicit special cases for the infinite loops.

An arithemetic expression under denotational semantics is a function that maps memory states to integers.

So, x+y could be thought of as function, if sigma1 is a memory state in which x maps to 5 and y maps to 112, the (x+y)applied to sigma1 would give the integer 117.

x==5 && y <=3  is mapped to a function that takes states to booleans.  If it is applied to a state in which x is 5 and y is 2, then this function applied to that state would give you the value true.

Arithmetic expressions map memory states to integers.
Boolean expressions map memory states to (true/false)
Commands "sort of" map memory to other memory states, sort of because some commands go into infinite loops.

Commands map SIGMA to SIGMAT.

We think of A (the stylized, italicized A) as taking an arithemetic expression and returning a function.  That function takes a memory state and returns an integer.

So, A[[x+y]] doesn't actually return a numeric value.  It returns a function and that function takes a memory state and returns an integer.

A[[x+y]] sigma(5/x,112,x) would give you integer 117.

Similarly, B[[x==5]] does not directly return a true or false value, it returns a function that takes states and returns a boolean value.

And C[[some command]] returns a function that maps memory states to memory states (plus infinite loop).

A[[n]] (sigma) = n,  where n is a constant.

A[[x]] (sigma) = sigma(x), where x is a variable

A[[expr1+expr2]] sigma = A[[expr1]](sigma) + A[[expr2]](sigma)
A[[expr1-expr2]] sigma = A[[expr1]](sigma) - A[[expr2]](sigma)
A[[expr1*expr2]] sigma = A[[expr1]](sigma) * A[[expr2]](sigma)

You can the boolean stuff similarly

B[[n]] (sigma) = n, where n is a true or false constant.
B[[expr1==expr2]] (sigma) = A[[expr1]](sigma) == A[[expr2]](sigma)

Define others similarly.

while (condition, maxloop):  if you make "maxloop" a necessary part of the loop construction so that the loop terminates after maxloop iterations even if the condition is still true, then you have eliminated infinite loops from the language.  "Maxloop" can be expressed in variables, but it is only computed once, at the onset of the loop.

But if you this, some problems can no longer be solved.

C[[skip]](sigma) = sigma.  In other words C[[skip]] returns the identity function.

C[[x:=expr]](sigma) = sigma [A[[expr]](sigma) / x]

C[[command1; command2]] (sigma) = C[[command2]]* (C[[command1]](sigma))

C[[command1]](sigma) MIGHT return an infinite loop, so we use the lifting notation.

C[[if b then command1 else command2]](sigma) =
B[[b]](sigma)->C[[command1]](sigma),C[[command2]](sigma)
This is their "lambda syntax" for if statements.

C[[while b do c]](sigma) =
B[[b]](sigma)->C[[while b do c]]* (C[[c]](sigma)),sigma

So, this describes what happens a loop.  If the boolean is true, we run the loop once, and then apply the entire while loop to the new state.