Structural induction is a technique that can be used to prove properties of the form "for all phrases p in a programming language L, the property P holds".
To prove that a property P holds for all phrases p, prove that, for all p, if P holds for all proper subphrases of p, then P holds for p.
The case where no proper subphrases exist is known as the base case, and the case where proper subphrases do exist is known as the inductive step. The assumption "P holds for all proper subphrases of p" is known as the induction hypothesis. We can think of structural induction as ordinary mathematical induction on the depth of syntax trees.
Here we will prove the claim that for
the SMC machine,
for all ⟨S, M, C⟩ and e there exists a c and M' such that
⟨S, M, e:C⟩⇒*⟨c:S, M', C⟩.
The proof is by structural induction on the expression to be evaluated. Any such expression has three possible forms:
| Expression Type | Example |
|---|---|
| Variable | xi |
| Constant | c |
| Composite | e1 op e2 |
Let us consider them in turn:
Base case variable:
Our start state is ⟨S, M, xi:C⟩ for some S, M and C.
From the rules of the SMC machine we have:
⟨S, M, xi:C⟩⇒⟨ci:S, M, C⟩
where M=c0,c1,c2,....
So the result holds in this case.
Base case constant:
Our start state is ⟨S, M, c:C⟩ for some S, M and C.
From the rules of the SMC machine we have:
⟨S, M, c:C⟩⇒⟨c:S, M, C⟩
So the result holds in this case.
Inductive step composite:
Our start state is ⟨S, M, (e1 op e2):C⟩
for some S, M and C.
From the rules of the SMC machine we have:
⟨S, M, (e1 op e2):C⟩⇒⟨S, M, e1:e2:op:C⟩
By the induction hypothesis we can assume the following:
⟨S, M, e1:e2:op:C⟩⇒*⟨c1:S, M'', e2:op:C⟩⟨c1:S, M'', e2:op:C⟩⇒*⟨c2:c1:S, M', op:C⟩
And from SMC rule for the operator we have
⟨c1:c2:S, M', op:C⟩⇒⟨c3:S, M', C⟩
So the result holds in this case.
Hence the result is established by structural induction.
Here we will prove the claim that the evaluation of expression on the SMC machine does not alter the memory.
The proof is by structural induction on the expression to be evaluated. Any such expression has three possible forms:
| Expression Type | Example |
|---|---|
| Variable | xi |
| Constant | c |
| Composite | e1 op e2 |
Let us consider them in turn:
Base case variable:
Our start state is ⟨S, M, xi:C⟩ for some S, M and C.
From the rules of the SMC machine we have:
⟨S, M, xi:C⟩⇒⟨ci:S, M, C⟩whereM=c0,c1,c2,...
As M is not altered, the result holds in this case.
Base case constant:
Our start state is ⟨S, M, c:C⟩ for some S, M and C.
From the rules of the SMC machine we have:
⟨S, M, c:C⟩⇒⟨c:S, M, C⟩
As M is not altered, the result holds in this case.
Inductive step composite:
Our start state is ⟨S, M, (e1 op e2):C⟩
for some S, M and C.
From the rules of the SMC machine we have:
⟨S, M, (e1 op e2):C⟩⇒⟨S, M, e1:e2:op:C⟩
By the induction hypothesis we can assume that the evaluation of
e1 and e2 does not alter the memory.
We also know from the proof in the previous example that e1 and e1 will
evaluate to some constants, say c1 and c2.
From this we have:
⟨S, M, e1:e2:op:C⟩⇒*⟨c:2:c1:S, M, op:C⟩.
And from SMC rule for the operator we have
⟨c1:c2:S, M, op:C⟩⇒⟨c3:S, M, C⟩
As M is not altered, the result holds in this case.
Hence the result is established by structural induction.
R. Burstall. Language Semantics and Implementation. Course Notes. 1994.
Copyright © 2014 Barry Watson. All rights reserved.