Index

Equivalence of Structured Transition and Relational Semantics Definitions (Proof)

We can prove the equivalence of the structured transition semantics and relational semantics definitions of a language. As an example language, we'll use IMP. Consider the following two semantic definitions.

Structured Transition Semantics for IMP

We now define a set of rules for the transition relation →∈(Phrases×Memories)×(Phrases×Memories).

Expressions

ConstantNo rules as ci is fully evaluated
Variablexi,M → ci,M where M=c0,c1,c2,...
Composite
  1.      e1,M → e'1,M'
    -----------------------
    e1 op e2,M → e'1 op e2,M'
  2.      e2,M → e'2,M'
    ------------------------
    n1 op e2,M → n1 op e'2,M'
  3. n1 op n2,M → n3,M, where n3 = n1 op n2

Programs

NullNo rules as null is fully evaluated
Assignment
  1.     e,M → e',M'
    -------------------
    xi:=e,M → xi:=e',M'
  2. xi:=n,M → null,M{n/i}
Sequence
  1.     p1,M → p'1,M'
    ----------------------
    (p1;p2),M → (p'1;p2),M'
  2. (null;p),M → p,M
Conditional
  1.              b,M → b',M'
    -------------------------------------------------
    if b then p1 else p2,M → if b' then p1 else p2,M'
  2. if true then p1 else p2,M → p1,M
  3. if false then p1 else p2,M → p2,M
Iteration while b do p,M → if b then (p;while b do p) else null,M

In the above, the notation M{n/i} means the ith memory value is set to n.

Relational Semantics for IMP

Our transition relation for IMP is ⇒⊆(Phrases×Memories)×Results. In the case of expressions, the set Results will be all elements of the form (c,M) where c is a constant and M is a memory. For programs, the set Results will be the set of memories. We can now define the terminal transition system (Γ,⇒,T) where Γ= Phrases×Memories∪T, T=Results, and γ⇒γ' implies that γ'∈Γ.

Expressions
Constant c,M ⇒ c,M
Variable xi,M ⇒ ci,M where M=c0,c1,...
Composite e1,M ⇒ n1,M' e2,M' ⇒ n2,M''
--------------------------
     e1 op e2,M ⇒ n3,M''      where n3=n1 op n2
Programs
Null null,M ⇒ M
Assignment   e,M ⇒ n,M'
-----------------
xi:=e,M ⇒ M'{n/i} Here M'{n/i} means memory location i contains value n.
Sequence p1,M ⇒ M' p2,M' ⇒ M''
----------------------
   (p1;p2),M ⇒ M''
Conditional
  1.   b,M ⇒ true,M' p1,M' ⇒ M''
    ----------------------------
    if b then p1 else p2,M ⇒ M''
  2.   b,M ⇒ false,M' p2,M' ⇒ M''
    ----------------------------
    if b then p1 else p2,M ⇒ M''
Iteration
  1. b,M ⇒ true,M' p,M' ⇒ M'' while b do p,M'' ⇒ M'''
    --------------------------------------------------
               while b do p,M ⇒ M'''
  2.    b,M ⇒ false,M'
    --------------------
    while b do p,M ⇒ M'

Equivalence Proof

We will prove the equivalence of

  1. e,M→*c,M' ⇔ e,M⇒c,M'
  2. p,M→*null,M' ⇔ p,M⇒M'

Proof of 1: e,M→*c,M' ⇔ e,M⇒c,M'

First we prove the ⇐ part which we do with structural induction on e,M⇒c,M'.

Case 1: e≡c. The ⇒ constant rule gives us M=M'. There is no → rule for this case as the expression is fully evaluated, i.e. we have c,M→*c,M in zero transitions.

Case 2: e≡xi. The ⇒ variable rule gives us c=ci and M=M'. From the → variable rule we easily see that the result holds in this case.

Case 3: e≡e1 op e2. By the ⇒ composite rule and the induction hypothesis we have e1,M→*n1,M' ⇐ e1,M⇒n1,M', and e2,M'→*n2,M'' ⇐ e2,M'⇒n2,M''. The → composite rules give us the desired result: e1 op e2,M→*n3,M''.

Hence the result is established by structural induction.

Now we prove the ⇒ part which we do with induction on the length of the computation e,M→*c,M'

Case 1: e≡c. In this case M=M' as there is no → rule, i.e. the computation takes zero transitions. From the ⇒ constant rule we see that the result holds in this case.

Case 2: e≡xi. The → variable rule Gives us c=ci and M=M'. From the ⇒ variable rule we see that the result holds in this case.

Case 3: e≡e1 op e2. Since e≡e1 op e2,M→*c,M', this must be inferred from the → composite rules with the following transitions:

  1. e1,M→*n1,M'
  2. e2,M'→*n2,M''
  3. n1 op n2,M''→n3,M'''

The list elements (1) and (2) above are computations of shorter length so by the induction hypothesis we have

  1. e1,M⇒n1,M'
  2. e2,M'⇒n2,M''

and by the ⇒ composite rule we see the result holds for this case.

Hence the result is established by induction on the length of computation.

Proof of 2: p,M→*null,M' ⇔ p,M⇒M'

First we prove the ⇐ part which we do with structural induction on p,M⇒null,M'.

Case 1: p≡null. In this case M=M' and we can easily deduce null,M→*M

Case 2: p≡xi:=e. We can infer p,M⇒M' from the assignment rule for ⇒, so M'=M'{n/i} and e=n. It follows from the proof of (1) that e,M→*n,M'' so by the assignment rule for → we have xi:=e,M→*null,M''{n/i}

Case 3: p≡(p1;p2). Since p1 and p2 are structurally simpler, we have by the induction hypothesis:

By the sequence rule for → we have (p1;p2)→*null,M'''

Case 4: p≡if b then p1 else p2. Since p1 and p2 are structurally simpler, we have by the induction hypothesis:

It follows from the proof of (1) that e,M→*n,M'' so by the conditional rule for → we have if b then p1 else p2→*null,M'''' where M''''=M''' or M''''=M''

Case 5: p≡while b do p. Since p is structurally simpler, we have by the induction hypothesis: p,M→*null,M' ⇐ p,M⇒M'. Also it follows from the proof of (1) that e,M→*n,M''. So by the iteration rule for →: 

while b then p,M→if b then (p;while b do p) else null,M

By the conditional rule for →: 

if b then (p;while b do p) else null,M→*(p;while b do p),M''

By the sequence rule for →: 

(p;while b do p),M''→*while b do p,M'''

Finally, by the induction hypothesis we have: 

while b do p,M'''→*null,M''''

Hence result established by structural induction.

Now we prove the ⇒ part which we do with induction on the length of the computation p,M→*null,M'

Case 1: p≡null. There is no → rule in this case so M=M'. By the ⇒ null rule we have null,M⇒M.

Case 2: p≡xi:=e. Since xi:=e,M→*null,M' can only be inferred from the → assignment rule, we have the following:

  1. xi:=e,M→*xi:=n,M'
  2. xi:=n,M'→null,M'{n/i}

From (1) and the first equivalence proof above we have e,M⇒n,M. By the ⇒ assignment rule we have xi:=e,M⇒M'{n/i}

Case 3: p≡(p1;p2). Since (p1;p2),M⇒*null,M' can only be inferred from the → sequence rule, we have the following:

  1. p1,M→*null,M''
  2. (null;p1),M''→p2,M''
  3. p2,M''→*null,M'

By the induction hypothesis on (1) and (3) we have: 

p1,M⇒M''
p2,M''⇒M'

and by the ⇒ sequence rule we have (p1;p2)⇒M'

Case 4: p≡if b then p1 else p2. Since if b then p1 else p2,M→*null,M' can only be inferred from the → conditional rules, we have the following:

  1. p1,M''→*null,M'
  2. b,M→c,M''
  3. p2,M''→*null,M'

By the induction hypothesis on (1) and (3) we have: 

p1,M''⇒M'
p2,M''⇒M'

So by the ⇒ conditional rules we have if b then p1 else p2,M⇒M'

Case 5: p≡while b do p. Since while b do p,M⇒*null,M' can only be inferred from the → iteration rule, we have the following: 

if b then (p;while b do p) else null,M→*null,M'

From the earlier equivalence proof we have b,M⇒c,M. Now, it must be the case that b,M''→*false,M'' for some M'', otherwise the iteration would not terminate. From the induction hypothesis we have 

p,M'⇒M''
while b do p,M''⇒M'''
null,M'⇒M'

By the ⇒ iteration rules we have while b do p,M⇒M'

References

R. Burstall. Language Semantics and Implementation. Course Notes. 1994.

Index

Copyright © 2014 Barry Watson. All rights reserved.