Rule Induction

The Rule Induction Principle

Statement

Let $R$ be a set of rules on $X$. Let $X_R$ be the set of derivable elements.

To prove $\forall x \in X_R. P(x)$: show that for every rule

$\frac{u_1 \quad \cdots \quad u_n}{v}$

if $P(u_i)$ holds for all premises $u_i$, then $P(v)$ holds.

Intuition

If every rule “preserves” property $P$ from premises to conclusion, and $P$ holds for all axioms (rules with no premises), then $P$ holds for all derivable elements.

Examinable Proof: Rule Induction is Valid

Theorem: If $S = \{x \in X : P(x)\}$ is closed under all rules in $R$, then $X_R \subseteq S$.

Proof:

Method: Induction on the height of derivations.

Base case (height $\leq 0$): No derivation has height $0$ (a derivation must be a tree with at least a root). Alternatively: axioms have height $1$, and $S$ contains all axiom conclusions since $S$ is closed under rules with no premises.

Inductive step: Suppose all derivations of height $\leq n$ have conclusions in $S$. Consider a derivation of height $n+1$ with conclusion $v$.

The derivation uses some rule $\frac{u_1 \quad \cdots \quad u_n}{v}$ where each $u_i$ is derived by a subtree of height $\leq n$.

By the induction hypothesis, each $u_i \in S$.

Since $S$ is closed under the rule, $v \in S$.

Conclusion: By induction, every derivable element is in $S$.

Equivalence of Characterisations

Two Characterisations of $X_R$

1. $X_R = \{x : x \text{ has a derivation using } R\}$
2. $X_R = \bigcap \{S : S \text{ closed under } R\}$

Proof of Equivalence

$(1 \subseteq 2)$: Every $S$ closed under $R$ contains all derivable elements (shown by induction on derivation height).

$(2 \subseteq 1)$: $X_R$ is itself closed under $R$ (union of rule applications preserves membership), and contains exactly the derivable elements.

The Recipe for Rule Induction

To prove $\forall x \in X_R. P(x)$:

1. For each axiom $\frac{}{a}$: verify $P(a)$ holds
2. For each rule $\frac{u_1 \quad \cdots \quad u_n}{v}$: assume $P(u_1), \ldots, P(u_n)$ and prove $P(v)$

This is the single most reusable proof template in this course.

Example: Balanced Parentheses

Rules

$\frac{}{\varepsilon} \qquad \frac{u \quad v}{u(v)}$

Define language $L_R$ with these rules.

Claim

Every $w \in L_R$ has balanced parentheses: #(’(’) = #(’)’) and every prefix has at least as many ’(’ as ’)’.

Proof by Rule Induction

Axiom: $\varepsilon$ has 0 ’(’ and 0 ’)’. Trivially balanced.

Rule: Assume $u$ and $v$ are balanced. Consider $u(v)$.

• Count: adds 1 ’(’ and 1 ’)’ to total from $u$ and $v$. Since $u, v$ balanced, total balanced.
• Prefix property: Any prefix is either:
  • A prefix of $u$ (balanced by IH)
  • $u$ itself (balanced by IH)
  • $u($ or $u(v'$ where $v'$ is a prefix of $v$ (still satisfies prefix property)

Example: Natural Numbers

Rules

$\frac{}{0} \qquad \frac{n}{S(n)}$

Claim: Every derived $n$ is either $0$ or $S(m)$ for some derived $m$

Proof:

• Axiom: $0$ is of the right form.
• Rule: $S(n)$ is of the right form (as successor of $n$).

When to Use Rule Induction

Use rule induction when:

1. The set is defined inductively by rules
2. The property $P$ should be preserved by rule application
3. You need to prove something about all derivable elements

Common applications:

• Properties of syntax trees
• Type preservation in programming languages
• Semantic equivalences
• Language properties

---

Summary

• Rule induction: if $S$ closed under $R$, then $X_R \subseteq S$
• Recipe: handle axioms, then each rule preserves $P$ from premises to conclusion
• Proof: induction on derivation height
• Fundamental proof technique for inductively defined sets