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.
We now define a set of rules for the transition relation →∈(Phrases×Memories)×(Phrases×Memories)
.
Constant  No rules as c_{i} is fully evaluated 
Variable  x_{i},M → c_{i},M where M=c_{0},c_{1},c_{2},... 
Composite 

Null  No rules as null is fully evaluated 
Assignment 

Sequence 

Conditional 

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 i
^{th} memory value is set to n
.
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  x_{i},M ⇒ c_{i},M where M =c_{0},c_{1} ,... 
Composite  e_{1},M ⇒ n_{1},M' e_{2},M' ⇒ n_{2},M''
where n_{3} =n_{1} op n_{2} 
Programs  
Null  null,M ⇒ M 
Assignment 
e,M ⇒ n,M'
Here M'{n/i} means memory location i contains value n .

Sequence 
p_{1},M ⇒ M' p_{2},M' ⇒ M''

Conditional 

Iteration 

We will prove the equivalence of
e,M→^{*}c,M'
⇔ e,M⇒c,M'
p,M→^{*}null,M'
⇔ p,M⇒M'
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≡x_{i}
.
The ⇒
variable rule
gives us c=c_{i}
and M=M'
.
From the →
variable rule
we easily see that the result holds in this case.
Case 3:
e≡e_{1} op e_{2}
.
By the ⇒
composite rule
and the induction hypothesis we have
e_{1},M→^{*}n_{1},M'
⇐ e_{1},M⇒n_{1},M'
, and
e_{2},M'→^{*}n_{2},M''
⇐ e_{2},M'⇒n_{2},M''
.
The →
composite rules
give us the desired result: e_{1} op e_{2},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≡x_{i}
.
The →
variable rule
Gives us c=c_{i}
and M=M'
.
From the ⇒
variable rule
we see that the result holds in this case.
Case 3:
e≡e_{1} op e_{2}
.
Since e≡e_{1} op e_{2},M→^{*}c,M'
, this must be inferred from the
→
composite rules
with the following transitions:
e_{1},M→^{*}n_{1},M'
e_{2},M'→^{*}n_{2},M''
n_{1} op n_{2},M''→n_{3},M'''
The list elements (1) and (2) above are computations of shorter length so by the induction hypothesis we have
e_{1},M⇒n_{1},M'
e_{2},M'⇒n_{2},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.
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≡x_{i}:=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 x_{i}:=e,M→^{*}null,M''{n/i}
Case 3:
p≡(p_{1};p_{2})
.
Since p_{1}
and p_{2}
are structurally simpler, we have by the induction hypothesis:
p_{1},M→^{*}null,M'
⇐ p_{1},M⇒M'
p_{2},M'→^{*}null,M''
⇐ p_{2},M'⇒M''
By the sequence rule for →
we have (p_{1};p_{2})→^{*}null,M'''
Case 4:
p≡if b then p_{1} else p_{2}
.
Since p_{1}
and p_{2}
are structurally simpler, we have by the induction hypothesis:
p_{1},M'→^{*}null,M''
⇐ p_{1},M'⇒M''
p_{2},M'→^{*}null,M'''
⇐ p_{2},M''⇒M'''
It follows from the proof of (1) that e,M→^{*}n,M''
so by the
conditional rule for →
we have
if b then p_{1} else p_{2}→^{*}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≡x_{i}:=e
.
Since x_{i}:=e,M→^{*}null,M'
can only be inferred from the
→
assignment rule, we have the following:
x_{i}:=e,M→^{*}x_{i}:=n,M'
x_{i}:=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 x_{i}:=e,M⇒M'{n/i}
Case 3:
p≡(p_{1};p_{2})
.
Since (p_{1};p_{2}),M⇒^{*}null,M'
can only be inferred from the
→
sequence rule, we have the following:
p_{1},M→^{*}null,M''
(null;p_{1}),M''→p2,M''
p_{2},M''→^{*}null,M'
By the induction hypothesis on (1) and (3) we have:
p_{1},M⇒M'' p_{2},M''⇒M'
and by the ⇒
sequence rule we have (p_{1};p_{2})⇒M'
Case 4:
p≡if b then p_{1} else p_{2}
.
Since if b then p_{1} else p_{2},M→^{*}null,M'
can only be inferred from the
→
conditional rules, we have the following:
p_{1},M''→^{*}null,M'
b,M→c,M''
p_{2},M''→^{*}null,M'
By the induction hypothesis on (1) and (3) we have:
p_{1},M''⇒M' p_{2},M''⇒M'
So by the ⇒
conditional rules we have if b then p_{1} else p_{2},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'
R. Burstall. Language Semantics and Implementation. Course Notes. 1994.
Copyright © 2014 Barry Watson. All rights reserved.