Structure of proof by induction in lambda calculus

inductionlambda-calculus

I want to prove some theorems in lambda calculus using induction on the length of the term.
Surprisingly, I haven't been able to find a single simple and complete proof online
that uses this approach.
Is the proof structure I have outlined below correct?
I've read Induction on the length of a $\lambda$-term, but it didn't go into detail on the inductive step, which is the part I'm unsure about.

The base case for this type of proof is $lgh(M) = 1$.
Proving the base case is simply proving that the theorem holds when $M$ is an atom.

For the inductive hypothesis, we assume that the theorem holds when $lgh(M) \lt n$.

Then we consider some $M$ where $lgh(M) = n$.
By the syntax of lambda calculus, the term $M$ must be
an atom, an application, or an abstraction.
We've already handled the base case where $M$ is an atom.
So now we have to consider the remaining two cases.

Case 1: $M$ is an application.
Let $M \equiv P Q$.
In proving this case, we can make use of the fact that
since $lgh(P) < n$ and $lgh(Q) < n$,
by the inductive hypothesis, the theorem holds for $P$ and $Q$.

Case 2: $M$ is an abstraction.
Let $M \equiv λy.P$
In proving this case, we can make use of the fact that
since $lgh(P) < n$,
by the inductive hypothesis, the theorem holds for $P$.

Once we've proved the base case, and cases 1 and 2, the proof by induction is complete.

Best Answer

You got the terms in IH and IS a bit mixed up. Your inductive base is correct. In the inductive hypothesis, you must assume that the property holds of all subterms you are going to use in the inductive step, i.e., $P$ and $Q$. In the inductive step, you must argue why, provided that the property holds for its subterms (= $\stackrel{IH}{...}$), it must also hold for the complex term $M$. And as the answer in the linked post notes, "induction on the length of" essentially means "structural induction on".

Here is an example showing that the number of parentheses in a lambda term is always even.

To show: For each $M \in \Lambda, paren(M) = 2m$ for some $m \in \mathbb{N}$.

Base case:
(i) $M \equiv v, v \in VAR$. $paren(v) = 0 = 2 \cdot 0$.
(ii) $M \equiv c, c \in CONST$. Analogous.

Induction hypothesis:
$paren(P) = 2p$ and $paren(Q) = 2q$ for some $p, q \in \mathbb{N}$.

Induction step:
(i) $M \equiv PQ.$ $paren(PQ) = paren(P) + paren(Q) \stackrel{IH}{=} 2p + 2q = 2(p+q)$.
(ii) $M \equiv (\lambda v. P)$. $paren((\lambda v.P)) = 2 + paren(P) \stackrel{IH}{=} 2 + 2p = 2(1+p).$

Q.E.D.

Graphically, you can imagine it like the following:

|IB |         IS       |
 M0    M1    M2    ...
  ╵----^╵----^
   P,Q    P,Q
       IH
Related Question