# 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.