Alpha conversion and free variables

Question

I am studying lambda calculus from "Lectures on the Curry-Howard isomorphism" and I want to clear out a small detail in a proof using induction on the definition of alpha conversion.

Alpha conversion is defined as:

The relation $=_{\alpha}$ ($\alpha$-conversion) is the least (i.e. smallest) transitive and reflexive relation on $\Lambda^{-}$ satisfying the following.

• If $y \notin FV ( M )$ and $M [ x := y ]$ is defined then $\lambda x M =_{\alpha} \lambda y . M [ x := y ]$.

• If $M =_{\alpha} N$ then $\lambda x M =_{\alpha} \lambda x N$, for all variables $x$.

• If $M =_{\alpha} N$ then $MZ =_{\alpha} NZ$.

• If $M =_{\alpha} N$ then $ZM =_{\alpha} ZN$.

After that there is the following lemma:

If $M=_a N$ then $FV(M)=FV(N)$. (a-equivalent lambda terms have the same free variables)

Using induction on the definition, the proof starts with the case of $M=_a N$ that follows from transitivity. i.e. $M=_aL$ and $L=_aN$.

THE QUESTION: What is the induction hypothesis in this step? Is it that "there exists a lambda term $L$ s.t. $M=_aL$ and $L=_aN$ and $FV(M)=FV(L)$, $FV(L)=FV(N)$? Is it something else that I am not able to find?

Answer 1

Given a relation $\sim$, its transitive-reflexive closure $\sim^*$ is usually defined:

• either by induction, saying that $M \sim^* M$ (reflexivity) and that if $M \sim N \sim^* P$ then $M \sim^* P$ (transitivity),
• or by indexing by integers (which is another form of induction of course) and saying that $M \sim^* N$ whenever there exists a sequence $M \sim M_1 \sim \dots \sim M_n \sim N$.

So when you want to prove something by induction on such a closure, you prove it:

• by structural induction with the first definition (one case for reflexivity, one case for transitivity),
• by induction on $n$ with the second definition, i.e. by induction “on the length of $M \sim^* N$” (again, one case for $n = 0$ and one case for $n \neq 0$, which are the same cases as above of course).

Your proof seems to use a variant of the first formalism:

$=_α$ is defined by structural induction, saying that

• if $M \sim N$ (for the inductively defined $\sim$ you give) then $M =_α N$,
• $M =_α M$ (reflexivity)
• if $M =_α N =_α P$ then $M =_α P$ (transitivity)

so you get three cases. In the case of transitivity, the induction hypothesis is the one you give. The case of reflexivity is immediate. The first case is showed by induction (with four sub-cases, corresponding to the inductive definition you give).

Of course, this can also be “flattened” into a single induction (instead of two nested ones), with six cases: the four cases of $\sim$, plus reflexivity and transitivity.