Induction on the length of computation is a technique that can be used to prove properties of transition systems.
To prove that a property P holds for all finite computations, prove that for all n ≥ 0, if P holds for all computations of length less than n then P holds for all computations of length n.
The case n=0 is known as the base case, and the case where n>0 is known as the inductive step. The assumption "P holds for all computations of length less than n" is known as the induction hypothesis.
Here we will prove the claim that if a configuration of the SMC machine starts in a state
⟨S, M, C⟩
where C
contains expressions and numeric operators only, and
⟨S, M, C⟩⇒^{*}⟨S', M', C'⟩
, then C'
contains expressions
and numeric operators only.
The proof is by induction on the length, k, of the computation
⟨S, M, C⟩⇒^{k}⟨S', M', C'⟩
Base case, k=0: Here ⟨S, M, C⟩=⟨S', M', C'⟩
so C'
contains
expressions and numeric operators only.
Inductive step, k>0: Consider a computation of length k:
⟨S, M, C⟩⇒^{k-1}⟨S'', M'', C''⟩⇒⟨S', M', C'⟩
We use the induction hypothesis on the computation of length k-1:
⟨S, M, C⟩⇒^{k-1}⟨S'', M'', C''⟩
So we assume that C''
contains expressions and numeric operators only. It remains to show that
the single step
⟨S'', M'', C''⟩⇒⟨S', M', C'⟩
gives a C'
which contains only expressions and numeric operators.
We do this by analysing each possible transition.
Since C''
contains only expressions and numeric operators, the only transition rules that are applicable
are the following:
Constant | ⟨S, M, c:C⟩⇒⟨c:S, M, C⟩ |
Variable | ⟨S, M, x_{i}:C⟩⇒⟨c_{i}:S, M, C⟩ where M=c_{0},c_{1},c_{2},... |
Composite | ⟨S, M, (e_{1} op e_{2}):C⟩⇒⟨S, M, e_{1}:e_{2}:op:C⟩ |
Operator | ⟨n_{1}:n_{2}:S, M, op:C⟩⇒⟨n_{3}:S, M, C⟩ where n_{3} is the evaluation of n_{1} op n_{2} |
We treat each of them in turn:
C''
=c:C
, S''
=S
, M''
=M
:⟨S, M, c:C⟩⇒⟨c:S, M, C⟩
,
so C'
=C
therefore C'
contains only expressions and numeric operators.
C''
=x_{i}:C
, S''
=S
, M''
=M
:⟨S, M, x_{i}:C⟩⇒⟨c_{i}:S, M, C⟩
where M=c_{0},c_{1},c_{2},...
,
so C'
=C
therefore C'
contains only expressions and numeric operators.
C''
=(e_{1} op e_{2}):C
, S''
=S
, M''
=M
:⟨S, M, (e_{1} op e_{2}):C⟩⇒⟨S, M, e_{1}:e_{2}:op:C⟩
,
so C'
= e_{1}:e_{2}:op:C
therefore C'
contains only expressions and numeric operators.
C''
=op:C
, S''
=n_{1}:n_{2}:S
, M''
=M
:⟨n_{1}:n_{2}:S, M, op:C⟩⇒⟨n_{3}:S, M, C⟩
where n_{3}
is the evaluation of n_{1} op n_{2}
so C'
=C
therefore C'
contains only expressions and numeric operators.
Hence the result is established by induction on the length of computation.
R. Burstall. Language Semantics and Implementation. Course Notes. 1994.
Copyright © 2014 Barry Watson. All rights reserved.