1. Induction

Proof by Induction

Proof by Induction consists of:

• Base Case: show that solution holds for $n=1$
• Inductive Case:
  1. Assume that it holds for $n=k$.
  2. Substitute to confirm it also holds for $n=k+1$.

Link to original

In the frame of this module, for any property $P(n)$ of natural numbers ($n\in \mathcal{N}=\{0,1,2,\dots \}$) to prove $\forall n\in \mathcal{N}.P(n)$ it is sufficient to show:

• Base Case: $P(0)$
• Induction Step: $\forall n\in \mathcal{N}.P(n)\Rightarrow P(n+1)$

Structural Induction

We denote an empty list by $nil$, and a non-empty list by $cons(h,l)$ where $h$ is the head element and $l$ is the tail of the list.

To prove a property $P$ holds for every list, it is sufficient to prove:

• Base Case: $P(nil)$
• Induction Step: $P(I)\Rightarrow P(cons(h,l))\text{ for all }h,l$.

More generally, if we are working with finite labelled trees and we want to prove a property $P$ for those trees, it is sufficient to show:

• Base Case: $P(I)\text{ for all leaf nodes }I$
• Induction Step: for each tree constructor $c$ (with $n\ge 1$ arguments): $\forall t_1,\dots ,t_n.P(t_1)\wedge \dots \wedge P(t_n)\Rightarrow P(c(t_1,\dots ,t_n))$

Example: to prove a property $P$ holds for all integer expressions in SIMP:

1. Base Case: prove $P(n)$ for all $n\in Z$, prove $P(!I)$ for all locations $I$.
2. Induction Step: for all integer expressions $E$, $E^{\prime }$ and operators $\text{op}$: Prove that $P(E)$ and $P(E^{\prime })$ implies $P(E\text{ op }{E}^{\prime })$.

Application of Structural Induction Principle

For example, we want to prove the property “the semantics of SIMP guarantees that for any integer expression $E$ appearing in a program working on a memory $m$, if $E$ uses locations that are defined in $m$ then the value of $E$ is defined”.

Or otherwise, for any configuration $⟨E\cdot c,r,m⟩$ where $c$ is any arbitrary control stack and $r$ is also arbitrary, there is a configuration $⟨c,n\cdot r,m⟩$ such that $⟨E\cdot c,r,m⟩{\to }^{\ast }⟨c,n\cdot r,m⟩$.

We have to prove $\forall E.P(E)$ where $P$ is:

$$\forall m.\text{locations}(E)\in dom(m)\Rightarrow \exists n.\forall c.\forall r.⟨E\cdot c,r,m⟩{\to }^{\ast }⟨c,n\cdot r,m⟩$$

This is proved by induction on the structure of $E$:

• Base Case: if $E$ is a number $n$ or $!I$ then the transitions for constants and locations prove $P(E)$
• Induction Step: assume $P(E_1)$ and $P(E_2)$ hold, we have to prove $P(E_1\text{ op }{E}_2)$.

Inductive Definitions

We can also use induction to define subsets of a given set $T$. We will write inductive definitions using axioms (representing the base case) and rules (representing the induction step).

A axiom is an element of $T$. A rule is a pair $(H,c)$ where:

• $H$ is a non-empty subset of $T$ called the hypotheses of the rule.
• $c$ is an element of $T$ called the conclusion of the rule.

The subset $I$ of $T$ inductively defined by a collection of axioms $A$ and rules $R$ consists of those $t\in T$ such that:

• $t\in A$
• there are $t_1,\dots ,t_n\in I$ and a rule $(H,c)$ such that $H=\{t_1,\dots ,t_n\}$ and $t=c$.

To show that an element $t$ of $T$ is in $I$ it is sufficient to show that $t$ is an axiom, or that there is a proof: Where the leaves are axioms and for each non-leaf node $t$, there is a rule $(\{t_{i1},\dots ,t_{i{m}_j}\},t_i)$. This proof is usually written:

Examples of Inductive Definitions

1. Natural Numbers Axiom: $0$ Rule: $(\{n\},n+1)$ Usually written as: $\frac{n}{n+1}$
2. Evaluation relation for integer expressions in SIMP Notation: $(E,m)\Downarrow n$ means $E$ evaluates to $n$ in state $m$. Axioms: $\begin{array}{rlr}(n,m)\Downarrow n& & \text{for all integer numbers }n\\ (!I,m)\Downarrow n& & \text{if }I\in dom(m)\text{ and }m(I)=n\end{array}$ Rule: $\frac{(E_1,m)\Downarrow n_1(E_2,m)\Downarrow n_2}{(E_1\text{ op }{E}_2,m)\Downarrow n}\text{ if }n=n_1\text{ op }{n}_2$

Rule Induction

We can write a principle of induction for this kind of inductive definition, called rule induction.

Principle of Rule Induction Let $I$ be a set defined by induction with axioms and rules $(A,R)$. To show that $P(i)$ holds for all $i\in I$, it is sufficient to prove:

• Base Case: $\forall a\in A.P(a)$
• Induction Step: $\forall (\{h_1,\dots ,h_n\},c)\in R.P(h_1)\wedge \dots \wedge P(h_n)\Rightarrow P(c)$

Example: each integer expression in SIMP has a unique value under the evaluation relation $\Downarrow$ Basis: trivial since numbers have unique values Induction Step: for non-atomic expressions, we remark that the value of an arithmetic expression is uniquely determined by the values of its arguments, which are unique by the induction hypotheses

Special Principle of Rule Induction In some cases, we are only interested in proving a property for a subset $J$ of the inductive set $I$ defined by $(A,R)$. Then we can use a special case of the principle of rule induction, which says that to prove that a property $Q(x)$ holds for all the elements of $J$, it is sufficient to show that:

• Basis: $\forall a\in (A\cup J).Q(a)$
• Induction Step: for all $(H,c)\in R$ such that $c\in J$, $(\forall h\in H\cap J.Q(h))\Rightarrow Q(c)$