# 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

 Constant No rules as `ci` is fully evaluated Variable `xi,M → ci,M` where `M=c0,c1,c2,...` Composite `     e1,M → e'1,M'` `-----------------------` `e1 op e2,M → e'1 op e2,M'` `     e2,M → e'2,M'` `------------------------` `n1 op e2,M → n1 op e'2,M'` `n1 op n2,M → n3,M`, where `n3 = n1 op n2`

### Programs

 Null No rules as `null` is fully evaluated Assignment `    e,M → e',M' ` `-------------------` `xi:=e,M → xi:=e',M' ` `xi:=n,M → null,M{n/i} ` Sequence `    p1,M → p'1,M'` `----------------------` `(p1;p2),M → (p'1;p2),M'` `(null;p),M → p,M` Conditional `             b,M → b',M'` `-------------------------------------------------` `if b then p1 else p2,M → if b' then p1 else p2,M'` `if true then p1 else p2,M → p1,M` `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 `i`th 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:

• `p1,M→*null,M'``p1,M⇒M'`
• `p2,M'→*null,M''``p2,M'⇒M''`

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:

• `p1,M'→*null,M''``p1,M'⇒M''`
• `p2,M'→*null,M'''``p2,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 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.