Induction On The Length Of Computation

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.

Example

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, xi:C⟩⇒⟨ci:S, M, C⟩ where M=c0,c1,c2,...
Composite	⟨S, M, (e1 op e2):C⟩⇒⟨S, M, e1:e2:op:C⟩
Operator	⟨n1:n2:S, M, op:C⟩⇒⟨n3:S, M, C⟩ where n3 is the evaluation of n1 op n2

We treat each of them in turn:

• Constant case C''=c:C, S''=S, M''=M:
  From the rule we have ⟨S, M, c:C⟩⇒⟨c:S, M, C⟩, so C'=C therefore C' contains only expressions and numeric operators.
• Variable case C''=xi:C, S''=S, M''=M:
  From the rule we have ⟨S, M, xi:C⟩⇒⟨ci:S, M, C⟩ where M=c0,c1,c2,..., so C'=C therefore C' contains only expressions and numeric operators.
• Composite case C''=(e1 op e2):C, S''=S, M''=M:
  From the rule we have ⟨S, M, (e1 op e2):C⟩⇒⟨S, M, e1:e2:op:C⟩, so C'= e1:e2:op:C therefore C' contains only expressions and numeric operators.
• Operator case C''=op:C, S''=n1:n2:S, M''=M:
  From the rule we have ⟨n1:n2:S, M, op:C⟩⇒⟨n3:S, M, C⟩ where n3 is the evaluation of n1 op n2 so C'=C therefore C' contains only expressions and numeric operators.

Hence the result is established by induction on the length of computation.

References

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