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.

Our lemma states that

e,x,n⇒_{s}e'∧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⇒`

and_{s}n''`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⇒`

and_{s}n`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≡e`

: From the substitution composite rule and the substitution semantics composite rule we have_{1}op e_{2}`e`

,_{1},x,n⇒_{s}e_{1}'`e`

,_{2},x,n⇒_{s}e_{2}'`e`

,_{1}'⇒n_{1}`e`

, and_{2}'⇒n_{2}`e`

where_{1}' op e_{1}'⇒n_{3}`n`

. From the induction hypothesis we have_{3}=n_{1}op n_{2}`{(x,n)}⊢e`

, and_{1}⇒n_{1}`{(x,n)}⊢e`

. From the environment semantics composite rule we can infer_{2}⇒n_{2}`{(x,n)}⊢e`

where_{1}op e_{2}⇒n_{3}`n`

._{3}=n_{1}op n_{2} - case
`e≡let x = e`

: From the first substitution let rule and the substitution semantics let rule we have_{0}in e_{1}`e`

,_{0},x,n⇒_{s}e_{0}'`let x = e`

,_{0}in e_{1}⇒_{s}let x = e_{0}' in e_{1}`e`

,_{0}'⇒n_{0}`e`

,_{1},x,n⇒_{s}e_{1}'`e`

, and_{1}'⇒n_{1}`let x = e`

. From the induction hypothesis we have_{0}in e_{1}⇒n_{1}`{(x,n)}⊢e`

, and_{0}⇒n_{0}`{(x,n)}⊢e`

. From the environment semantics let rule we can infer that_{1}⇒n_{1}`{(x,n)}⊢let x = e`

_{0}in e_{1}⇒n_{1} - case
`e≡let x' = e`

where_{0}in e_{1}`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⇒`

and_{s}n''`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⇒`

and_{s}n`n⇒n`

. - case
`e≡x'`

where`x≠x'`

: This case cannot occur. - case
`e≡e`

: From the environment semantics composite rule we have_{1}op e_{2}`{(x,n)}⊢e`

,_{1}⇒n_{1}`{(x,n)}⊢e`

, and_{2}⇒n_{2}`{(x,n)}⊢e`

where_{1}op e_{2}⇒n_{3}`n`

. From the induction hypothesis we have_{3}=n_{1}op n_{2}`e`

,_{1},x,n⇒_{s}e_{1}'`e`

,_{2},x,n⇒_{s}e_{2}'`e`

,_{1}'⇒n_{1}`e`

, and from the substitution semantics composite rule we can infer_{2}'⇒n_{2}`e`

where_{1}' op e_{1}'⇒n_{3}`n`

._{3}=n_{1}op n_{2} - case
`e≡let x = e`

: From the substitution semantics composite rule we have_{0}in e_{1}`{(x,n)}⊢e`

,_{0}⇒n_{0}`{(x,n)}⊢e`

, and_{1}⇒n_{1}`{(x,n)}⊢let x = e`

. From the induction hypothesis we have_{0}in e_{1}⇒n_{1}`e`

,_{0},x,n⇒_{s}e_{0}'`let x = e`

,_{0}in e_{1}⇒_{s}let x = e_{0}' in e_{1}`e`

,_{0}'⇒n_{0}`e`

,_{1},x,n⇒_{s}e_{1}'`e`

. From the substitution semantics let rule we can infer_{1}'⇒n_{1}`let x = e`

._{0}in e_{1}⇒n_{1} - case
`e≡let x' = e`

where_{0}in e_{1}`x≠x'`

: This is similar to the previous case.

Hence the result is established by structural induction.

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≡e`

: We have_{1}op e_{2}`e`

,_{1}⇒n_{1}`e`

,_{2}⇒n_{2}`e`

where_{1}op e_{2}⇒n_{3}`n3=n1 op n2`

. We use the induction hypothesis on the operands which gives us`{}⊢e`

,_{1}⇒n_{1}`{}⊢e`

. From the composite rule we infer_{2}⇒n_{2}`{}⊢e`

where_{1}op e_{2}⇒n_{3}`n3=n1 op n2`

. - case
`e≡let x = e`

: We have_{0}in e_{1}`e`

,_{0}⇒n_{0}`e`

, and_{1},x,n_{0}⇒_{s}e_{1}'`e`

From the induction hypothesis and the lemma we have_{1}',⇒n_{1}`{}⊢e`

,_{0}⇒n_{0}`{(x,n`

. From the let rule we can infer that_{0}}⊢e_{1}⇒n_{1}`{}⊢let x = e`

_{0}in e_{1}⇒n_{1}

- 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`{}⊢e`

. From the induction hypothesis we have_{0}⇒n`e`

. From the let rule we have_{0}⇒n`e`

. From the substitution rule for variable we have_{1},x,n⇒_{s}e_{1}'`x,x,n⇒`

._{s}n - case
`e≡e`

: We have_{1}op e_{2}`{}⊢e`

,_{1}⇒n_{1}`{}⊢e`

, and_{2}⇒n_{2}`{}⊢e`

where_{1}op e_{2}⇒n_{3}`n3=n1 op n2`

. We use the induction hypothesis on the operands which gives us`e`

,_{1}⇒n_{1}`e`

. From the composite rule we infer_{2}⇒n_{2}`e`

where_{1}op e_{2}⇒n_{3}`n3=n1 op n2`

. - case
`e≡let x = e`

: We have_{0}in e_{1}`{}⊢e`

,_{0}⇒n_{0}`{(x,n`

, and_{0}}⊢e_{1}⇒n_{1}`{}⊢let x = e`

. From the induction hypothesis and the lemma we have_{0}in e_{1}⇒n_{1}`e`

,_{0}⇒n_{0}`e`

, and_{1},x,n_{0}⇒_{s}e_{1}'`e`

. From the let rule we can infer that_{1}',⇒n_{1}`let x = e`

._{0}in e_{1}⇒n_{1}

Hence the result is established by structural induction.

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

Copyright © 2014 Barry Watson. All rights reserved.