EQUIVALENCE OF OPERATIONAL AND DENOTATIONAL SEMANTICS

The point is to show that these semantics describe a language in the same way.

<c,sigma> -> sigma'  [Operational] <==> C[[c]](sigma) = sigma' [Denotational]

==>:  Proof of correctness
<==:  Proof of completeness

STRUCTURAL INDUCTION, which is a lot like regular induction.  When we build a command from another commands(s), we assume that the semantics are identical from the smaller commands.  Now, we have axiomatic commands (base cases).  And the commands that build from them are sequence, if/then/else, and while.

Base cases:  <skip,sigma> -> sigma'  <==> C[[skip]](sigma) = sigma'.

==>:

______________________
<skip,sigma> -> sigma

This lets us know that the sigma' we're looking for is sigma.  Since we know that C[[skip]](sigma) is also sigma, this is true.

==>:  We know that C[[skip]](sigma) = sigma, so that's sigma is sigma'.  And we derive axiomatically that <skip,sigma> -> sigma.

Assignment:

<x:=a,sigma>-> sigma'   <=> C[[x:=a]](sigma) = sigma'.

<a,sigma>->n
________________________
<x:=a,sigma>->sigma(n/x)

if <a,sigma>->n  , this means A[[a]](sigma)=n.

C[[x:=a]](sigma) = sigma (A[[a]](sigma)/x).  (definition of assignment).
 = sigma (n/x).  And so the sigma' on right side is the same as the sigma prime on the left.

<==:

If we're given C[[x:=a]](sigma) = sigma'.  Then sigma' must be
sigma[A[[a]](sigma)/x].

Under the assumption that <a,sigma>->n, and knowing that A[[a]](sigma) = n, we can conclude that <x:=a,sigma>->sigma[A[[a]](sigma)/x] which is same as sigma[n/x].

sequence:

<c1;c2,sigma> -> sigma'  <=>  C[[c1;c2]](sigma) = sigma'.

C[[c1;c2]](sigma) = C[[c2]](C[[c1]](sigma))

<c1,sigma>-> sigma''  <c2,sigma''> -> sigma'
_____________________________________________
<c1;c2,sigma>-> sigma'

==>:

Structural induction:  <c1,sigma> -> sigma'' <==> C[[c1]](sigma) = sigma''.

This tells me that C[[c1]](sigma) = sigma''.
And that C[[c2]](sigma'') = sigma'.
C[[c2]](C[[c1]](sigma)) = C[[c2]](sigma'') = sigma'.
This side is proven, since our operational allowed us to derive sigma', and that was the answer in denotational semantics.

<==:

Assume C[[c1;c2]](sigma) = sigma'.

We now C[[c1]](sigma) has some sort of answer, (and it's not an infinite loop since we got an answer for c1;c2).  So, call that answer sigma''.

We have C[[c1]](sigma) = sigma''.
We C[[c1;c2]](sigma) = C[[c2]]((C[[c1]])(sigma)) = C[[c2]](sigma'') = sigma'.

Now we can derive our operational syntax.

Assume <c1,sigma>->sigma'' and that <c2,sigma''> -> sigma'.

Then from structural induction, C[[c1]](sigma) = sigma''.  C[[c2]](sigma'') = sigma'.  We know that C[[c1;c2]](sigma) = sigma'.

So we have derived that <c1;c2,sigma> -> sigma'.

if-then-else

Operational:

<b,sigma> -> false  <c2,sigma>->sigma'
______________________________________
<if b then c1 else c2> -> sigma'

<b,sigma> -> true  <c1,sigma>->sigma'
______________________________________
<if b then c1 else c2> -> sigma'

Denotational:
C[[if b then c1 else c2]](sigma) =
B[[b]] (C[[c1]],sigma),(C[[c2]],sigma)

==>:if B[[b]](sigma) = false then <b,sigma>->false (structural induction) and if C[[c2]],sigma) goes to,say, sigma', then <c2,sigma>->sigma' (structural induction)

Then from operational semantics we can derive sigma' from <if b then c1 else c2>.  Which is also the answer from B[[b]] (C[[c1]],sigma),(C[[c2]],sigma), since b evaluates to false.

if B[[b]](sigma) = true then <b,sigma>->true (structural induction) and if C[[c1]],sigma) goes to,say, sigma', then <c1,sigma>->sigma' (structural induction)

Then from operational semantics (the second rule) we can derive sigma' from <if b then c1 else c2>.  Which is also the answer from B[[b]] (C[[c1]],sigma),(C[[c2]],sigma), since b evaluates to true.

<==:  Assume denotational semantics are true

C[[if b then c1 else c2]](sigma) =
B[[b]] (C[[c1]],sigma),(C[[c2]],sigma)

We will try to derive the inference rules.

So, assume <b,sigma> -> true   and <c2,sigma> -> sigma'.

Then B[[b]] must be true (structural induction)

So, B[[b]] (C[[c1]],sigma),(C[[c2]],sigma) evaluates to C[[c1]](sigma).

From structural induction, since <c2,sigma> -> sigma'.  Then C[[c1]](sigma) = sigma'.

So, C[[if b then c1 else c2]](sigma) = sigma'.

<if b then c1 else c2,sigma>->sigma'.

And, assume <b,sigma> -> false   and <c2,sigma> -> sigma'.

Then B[[b]] must be false (structural induction)

So, B[[b]] (C[[c1]],sigma),(C[[c2]],sigma) evaluates to C[[c2]](sigma).

From structural induction, since <c2,sigma> -> sigma'.  Then C[[c2]](sigma) = sigma'.

So, C[[if b then c1 else c2]](sigma) = sigma'.

<if b then c1 else c2,sigma>->sigma'.

while:

<b,sigma>->false
___________________________
<while b do c,sigma>->sigma

<b,sigma>->true  <c,sigma>->sigma'' <while b do c,sigma''>->sigma'
__________________________________________________________________
<while b do c, sigma>->sigma'.

Denotational:

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