# Equivalence of Substitution Based Dynamic and Environment Based Dynamic Semantics (proof)

We can prove the equivalence of substitution based dynamic semantics and environment based dynamic semantics with a structural induction proof. Before we can prove this, our main result, we need to prove a lemma.

## Lemma

Our lemma states that

```e,x,n⇒se'∧e'⇒n' ⇔ {(x,n)}⊢e⇔n'
```

Which means that substituting a number, `n`, for a variable, `x`, in an expression will give the same result when evaluated with the substitution semantics as if the appropriate pair, `(x,n)`, was in the environment and the expression was evaluated with the environment semantics. The proof is a simple one by structural induction on the expression `e`.

### (⇒)

• case `e≡n''`: From the substitution number rule, and the substitution semantics number rule we have `n'',x,n⇒sn''` and `n''⇒n''`. From the environment semantics number rule we have `{(x,n)}⊢n''⇒n''`.
• case `e≡x`: From the first substitution variable rule and the substitution semantics number rule we have `x,x,n⇒sn` and `n⇒n` From the environment semantics variable rule we have `{(x,n)}⊢x⇒n`.
• case `e≡x'` where `x≠x'`: This case cannot occur.
• case `e≡e1 op e2`: From the substitution composite rule and the substitution semantics composite rule we have `e1,x,n⇒se1'`, `e2,x,n⇒se2'`, `e1'⇒n1`, `e2'⇒n2`, and `e1' op e1'⇒n3` where `n3=n1 op n2`. From the induction hypothesis we have `{(x,n)}⊢e1⇒n1`, and `{(x,n)}⊢e2⇒n2`. From the environment semantics composite rule we can infer `{(x,n)}⊢e1 op e2⇒n3` where ```n3=n1 op n2 ```.
• case `e≡let x = e0 in e1`: From the first substitution let rule and the substitution semantics let rule we have `e0,x,n⇒se0'`, `let x = e0 in e1⇒slet x = e0' in e1`, `e0'⇒n0`, `e1,x,n⇒se1'`, `e1'⇒n1`, and `let x = e0 in e1⇒n1`. From the induction hypothesis we have `{(x,n)}⊢e0⇒n0`, and `{(x,n)}⊢e1⇒n1`. From the environment semantics let rule we can infer that `{(x,n)}⊢let x = e0 in e1⇒n1`
• case `e≡let x' = e0 in e1` where `x≠x'`: This is similar to the previous case.

### (⇐)

• case `e≡n''`: From the environment semantics number rule we have we have `{(x,n)}⊢n''⇒n''`. From the substitution number rule, and the substitution semantics number rule we have `n'',x,n⇒sn''` and `n''⇒n''`.
• case `e≡x`: From the environment semantics variable rule we have we have `{(x,n)}⊢x⇒n`. From the first substitution variable rule and the substitution semantics number rule we have `x,x,n⇒sn` and `n⇒n`.
• case `e≡x'` where `x≠x'`: This case cannot occur.
• case `e≡e1 op e2`: From the environment semantics composite rule we have `{(x,n)}⊢e1⇒n1`, `{(x,n)}⊢e2⇒n2`, and `{(x,n)}⊢e1 op e2⇒n3` where `n3=n1 op n2`. From the induction hypothesis we have `e1,x,n⇒se1'`, `e2,x,n⇒se2'`, `e1'⇒n1`, `e2'⇒n2`, and from the substitution semantics composite rule we can infer `e1' op e1'⇒n3` where `n3=n1 op n2`.
• case `e≡let x = e0 in e1`: From the substitution semantics composite rule we have `{(x,n)}⊢e0⇒n0`, `{(x,n)}⊢e1⇒n1`, and `{(x,n)}⊢let x = e0 in e1⇒n1`. From the induction hypothesis we have `e0,x,n⇒se0'`, `let x = e0 in e1⇒slet x = e0' in e1`, `e0'⇒n0`, `e1,x,n⇒se1'`, `e1'⇒n1`. From the substitution semantics let rule we can infer `let x = e0 in e1⇒n1`.
• case `e≡let x' = e0 in e1` where `x≠x'`: This is similar to the previous case.

Hence the result is established by structural induction.

## Main Proof

Our main claim is that

```	∀e∈Exp,x∈Var,n∈N: e⇒n ⇔ {}⊢e⇒n
```

The proof is a simple one by structural induction on the expression `e`.

### (⇒)

• case `e≡n`: We have `n⇒n`. From the rule for numbers we have `{}⊢n⇒n`
• case `e≡x`: This case cannot occur.
• case `e≡e1 op e2`: We have `e1⇒n1`, `e2⇒n2`, `e1 op e2⇒n3` where `n3=n1 op n2`. We use the induction hypothesis on the operands which gives us `{}⊢e1⇒n1`, `{}⊢e2⇒n2`. From the composite rule we infer `{}⊢e1 op e2⇒n3` where `n3=n1 op n2`.
• case `e≡let x = e0 in e1`: We have `e0⇒n0`, `e1,x,n0⇒se1'`, and `e1',⇒n1` From the induction hypothesis and the lemma we have `{}⊢e0⇒n0`, `{(x,n0}⊢e1⇒n1`. From the let rule we can infer that `{}⊢let x = e0 in e1⇒n1`

### (⇐)

• case `e≡n`: We have `{}⊢n⇒n`. From the rule for numbers we have `n⇒n`
• case `e≡x`: We have `{E}⊢x⇒n` if `(x,n)∈E`. Because variables do not occur as expressions in the substitution semantics, the variable must have been substituted via the let rule. This also means that in the let rule for the environment semantics we have `{}⊢e0⇒n`. From the induction hypothesis we have `e0⇒n`. From the let rule we have `e1,x,n⇒se1'`. From the substitution rule for variable we have `x,x,n⇒sn`.
• case `e≡e1 op e2`: We have `{}⊢e1⇒n1`, `{}⊢e2⇒n2`, and `{}⊢e1 op e2⇒n3` where `n3=n1 op n2`. We use the induction hypothesis on the operands which gives us `e1⇒n1`, `e2⇒n2`. From the composite rule we infer `e1 op e2⇒n3` where `n3=n1 op n2`.
• case `e≡let x = e0 in e1`: We have `{}⊢e0⇒n0`, `{(x,n0}⊢e1⇒n1`, and `{}⊢let x = e0 in e1⇒n1`. From the induction hypothesis and the lemma we have `e0⇒n0`, `e1,x,n0⇒se1'`, and `e1',⇒n1`. From the let rule we can infer that `let x = e0 in e1⇒n1`.

Hence the result is established by structural induction.

## References

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