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⇒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.
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''.
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.
e≡x' where x≠x': This case cannot occur.
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
.
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
e≡let x' = e0 in e1 where x≠x':
This is similar to the previous 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''.
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.
e≡x' where x≠x': This case cannot occur.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.
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.
e≡let x' = e0 in e1 where 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.
e≡n: We have n⇒n.
From the rule for numbers we have {}⊢n⇒ne≡x: This case cannot occur.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.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
e≡n: We have {}⊢n⇒n.
From the rule for numbers we have n⇒ne≡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.
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.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.
R. Burstall. Language Semantics and Implementation. Course Notes. 1994.
Copyright © 2014 Barry Watson. All rights reserved.