Induction on the length of a $\lambda$-term

Question

I'm a bit confused about a statement that I see often in the $\lambda$-calculus literature. Namely, what exactly does the following statement mean: "By induction on the length of $M\in\Lambda$." ?

In such literature, $\Lambda$ is defined as the smallest subset of $\mathcal{V}\cup\{(,),\lambda\}$ such that:

• $x\in\Lambda$, if $x\in\mathcal{V}$
• $(PQ)\in\Lambda$, if $P,Q\in\Lambda$
• $(\lambda x P)\in\Lambda$, if $x\in\mathcal{V}$ and $P\in\Lambda$

where $\mathcal{V}$ is any fixed infinite set of symbols.

Now, the length of $M\in\Lambda$ is given by:

• $|x| = 1$
• $(PQ)$ = $|P|+|Q|$
• $(\lambda x P)$ = $1+|P|$

Therefore, my question is: in what way is "structural induction over $\Lambda$" any different than "induction on the length of a $\lambda$-term"? In particular, what is the inductive hypothesis in such inductive method?

Answer 1

For induction on length inductive hypothesis is that statement holds for lambda term of length n. Induction step is to infer that statement holds for lambda term of length n + 1 when it holds for lambda term of length n.

Structural induction is described in this topic $\lambda$-calculus: structural induction principle over $\Lambda$ and it is something different. Structural induction described in that topic is some specific case of induction on length.

Answer 2

As a practical matter the technique of structural induction and the technique of induction on length turn out to be the same, and you can take "induction on the length of the term" to be synonymous with "structural induction on the term".

In more detail, what is meant here is actually strong induction on the length of the term. The induction hypothesis is that some predicate $\Phi$ holds for all terms of length strictly less than $n$, and the inductive step uses the hypothesis to show that it must also hold for all terms of length $n$.

In practice this nearly always takes the form of a structural induction argument, something like this:

We want to show $\Phi(T)$, where $T$ has length $n$. Let $S$ be any proper subterm of $T$. Then since the length of $S$ is strictly less than the length of $T$, we know by the induction hypothesis that $\Phi(S)$…(etc.).

The "length" might be a structural length that counts the subterms, as the one in your question, or it could be the actual number of symbols in the λ-term:

$\def\size#1{\left|#1\right|}$

$$ \begin{align} \size v & = 1 \\ \size{\lambda x.T} & = 3 + \size T \\ \size{(PQ)} & = 2 + \size P + \size Q \end{align}$$

The details are unimportant. The important thing here is just that the size function $\size\cdot$ is strictly monotonic: we must have $\size S \lt\size T$ whenever $S$ is a subterm of $T$.