3.3 Induction on Terms

---

3.3 Induction on Terms

The explicit characterization of the set of terms T in Proposition 3.2.6 justifies an important principle for reasoning about its elements. If t Î T, then one of three things must be true about t: (1) t is a constant, or (2) t has the form succ t₁, pred t₁, or iszero t₁ for some smaller term t₁, or (3) t has the form if t₁ then t₂ else t₃ for some smaller terms t₁, t₂, and t₃. We can put this observation to work in two ways: we can give inductive definitions of functions over the set of terms, and we can give inductive proofs of properties of terms. For example, here is a simple inductive definition of a function mapping each term t to the set of constants used in t.

3.3.1 Definition

The set of constants appearing in a term t, written Consts(t), is defined as follows:

Consts(true)	=	{true}
Consts(false)	=	{false}
Consts(0)	=	{0}
Consts(succ t1)	=	Consts(t1)
Consts(pred t1)	=	Consts(t1)
Consts(iszero t1)	=	Consts(t1)
Consts(if t1 then t2 else t3)	=	Consts(t1) È Consts(t2) È Consts(t3)

Another property of terms that can be calculated by an inductive definition is their size.

3.3.2 Definition

The size of a term t, written size(t), is defined as follows:

size(true)	=	1
size(false)	=	1
size(0)	=	1
size(succ t1)	=	size(t1) + 1
size(pred t1)	=	size(t1) + 1
size(iszero t1)	=	size(t1) + 1
size(if t1 then t2 else t3)	=	size(t1) + size(t2) + size(t3) + 1

That is, the size of t is the number of nodes in its abstract syntax tree. Similarly, the depth of a term t, written depth(t), is defined as follows:

depth(true)	=	1
depth(false)	=	1
depth(0)	=	1
depth(succ t1)	=	depth(t1) + 1
depth(pred t1)	=	depth(t1) + 1
depth(iszero t1)	=	depth(t1) + 1
depth(if t1 then t2 else t3)	=	max(depth(t1), depth(t2), depth(t3)) + 1

Equivalently, depth(t) is the smallest i such that t Î S_i according to Definition 3.2.3.

Here is an inductive proof of a simple fact relating the number of constants in a term to its size. (The property in itself is entirely obvious, of course. What's interesting is the form of the inductive proof, which we'll see repeated many times as we go along.)

3.3.3 Lemma

The number of distinct constants in a term t is no greater than the size of t (i.e., |Consts(t)| ≤ size(t)).

Proof: By induction on the depth of t. Assuming the desired property for all terms smaller than t, we must prove it for t itself. There are three cases to consider:

Case:

t is a constant

Immediate: |Consts(t)| = |{t}| = 1 = size(t).

Case:

t = succ t₁, pred t₁, or iszero t₁

By the induction hypothesis, |Consts(t₁)| ≤ size(t₁). We now calculate as follows: |Consts(t)| = |Consts(t₁)| ≤ size(t₁) < size(t).

Case:

t = if t₁ then t₂ else t₃

By the induction hypothesis, |Consts(t₁)| ≤ size(t₁), |Consts(t₂)| ≤ size(t₂), and |Consts(t₃)| ≤ size(t₃). We now calculate as follows:

|Consts(t)|	=	|Consts(t1) È Consts(t2) È Consts(t3)|
	≤	|Consts(t1)| + |Consts(t2)| + |Consts(t3)|
	≤	size(t1) + size(t2) + size(t3)
	<	size(t).

The form of this proof can be clarified by restating it as a general reasoning principle. For good measure, we include two similar principles that are often used in proofs about terms.

3.3.4 Theorem [Principles of Induction on Terms]

Suppose P is a predicate on terms.

• Induction on depth:

  • If, for each term s,

    • given P(r) for all r such that depth(r) < depth(s)

    • we can show P(s),

  • then P(s) holds for all s.

• Induction on size:

  • If, for each term s,

    • given P(r) for all r such that size(r) < size(s)

    • we can show P(s),

  • then P(s) holds for all s.

• Structural induction:

  • If, for each term s,

    • given P(r) for all immediate subterms r of s

    • we can show P(s),

  • then P(s) holds for all s.

Proof: Exercise (⋆⋆).

Induction on depth or size of terms is analogous to complete induction on natural numbers (2.4.2). Ordinary structural induction corresponds to the ordinary natural number induction principle (2.4.1) where the induction step requires that P(n + 1) be established from just the assumption P(n).

Like the different styles of natural-number induction, the choice of one term induction principle over another is determined by which one leads to a simpler structure for the proof at hand—formally, they are inter-derivable. For simple proofs, it generally makes little difference whether we argue by induction on size, depth, or structure. As a matter of style, it is common practice to use structural induction wherever possible, since it works on terms directly, avoiding the detour via numbers.

Most proofs by induction on terms have a similar structure. At each step of the induction, we are given a term t for which we are to show some property P, assuming that P holds for all subterms (or all smaller terms). We do this by separately considering each of the possible forms that t could have (true, false, conditional, 0, etc.), arguing in each case that P must hold for any t of this form. Since the only parts of this structure that vary from one inductive proof to another are the details of the arguments for the individual cases, it is common practice to elide the unvarying parts and write the proof as follows.

Proof: By induction on t.

Case:	t = true
... show P(true) ...
Case:	t = false
... show P(false) ...
Case:	t = if t1 then t2 else t3
... show P(if t1 then t2 else t3), using P(t1), P(t2), and P(t3) ...

(And similarly for the other syntactic forms.)

For many inductive arguments (including the proof of 3.3.3), it is not really worth writing even this much detail: in the base cases (for terms t with no subterms) P(t) is immediate, while in the inductive cases P(t) is obtained by applying the induction hypothesis to the subterms of t and combining the results in some completely obvious way. It is actually easier for the reader simply to regenerate the proof on the fly (by examining the grammar while keeping the induction hypothesis in mind) than to check a written-out argument. In such cases, simply writing "by induction on t" constitutes a perfectly acceptable proof.

---