alpha equivalence of lambda calculus

Question

I am pretty new in λ calculus. And I am now trying to understand Alpha equivalence. Basically can I think it in this way: as long as I make sure all the bound variables and their corresponding abstractions are noted as the same letter, the new expression is alpha equivalent to the old one? Here is one example:

 (λx.(λx.x(λy.x)x)x)x

And by applying alpha equivalnce I can rewrite it to:

  (λw.(λz.w(λy.z)z)w)x

Is my understanding correct ?

Answer 1

Here is one example:

 (λx.(λx.x(λy.x)x)x)x

And by applying alpha equivalnce I can rewrite it to:

 (λw.(λz.w(λy.z)z)w)x

Is my understanding correct ?

There is a small error in your rewriting: at λz.w you have changed the meaning of the expression, because now the bound variable refers to the outer lambda abstraction, instead of the inner lambda abstraction as before. Instead, it should be λz.z. Other than this, the rewriting is correct.

Basically can I think it in this way: as long as I make sure all the bound variables and their corresponding abstractions are noted as the same letter, the new expression is alpha equivalent to the old one?

Yes, this understanding is correct.

Answer 2

One way to not mess up with variable names in $\lambda$-calculus is to use De Brujin indexes. With this, $\alpha$-equivallence becomes a really obvious syntactic equality, for instance:

\begin{align*} \lambda x.x &\rightarrow \lambda.0 \\ \lambda z.z &\rightarrow \lambda.0 \\ \lambda x .\lambda y. x &\rightarrow \lambda.\lambda.1 \\ \end{align*}

Intuitively, these indexes can be though as the number of $\lambda$s you have to skip to make a variable bound.

\begin{align*} \Bigg(λx.\Big(λx.x(λy.x)x\Big)x\Bigg)x &\rightarrow (\color{blue}{λx}.(\color{red}{λx}.\color{red}{x} (\color{green}{λy}.\color{red}{x})\color{red}{x})\color{blue}{x})\color{blue}{x} \\ (\color{blue}{λ}.(\color{red}{λ}.\color{red}{0} (\color{green}{λ}.\color{red}{1})\color{red}{0})\color{blue}{0})\color{blue}{0} &\rightarrow (λ.(λ.0(λ.1)0)0)0 \\ \end{align*}

And by applying alpha equivalnce I can rewrite it to:

(λw.(λz.w(λy.z)z)w)x

Is my understanding correct ?

Let's check:

\begin{align*} \Bigg(λw.\Big(λz.w(λy.z)z\Big)w\Bigg)x &\rightarrow (\color{blue}{λw}.(\color{red}{λz}.\color{blue}{w}(\color{green}{λy}.\color{red}{z})\color{red}{z})\color{blue}{w})\color{blue}{x} \\ (\color{blue}{\lambda}.(\color{red}{\lambda}.\color{blue}{1}(\color{green}{\lambda}.\color{red}{1})\color{red}{0})\color{blue}{0})\color{blue} {0} &\rightarrow (\lambda.(\lambda.1(\lambda.1)0)0)0 \end{align*}

Nope.