Brackets in Lambda Calculus with multiple lambdas

Question

How would you evaluate $\lambda x.\lambda x.\lambda x.x 1 2 3$? I cant figure out if the first lambda takes the 1 beta reduces, then the second lambda takes the 2 then beta reduces and finally the third lambda takes the 3 and beta reduces or if it goes the opposite way around. Pretty much my question is which lambda takes in which number and would the answer to this be 1 or 3?

Answer 1

That depends on your bracketing conventions, but I suppose that by

$$\lambda x. \lambda x. \lambda x.x123$$ you mean $$(\lambda x. \lambda x. \lambda x.x)123$$ which is shorthand for $$(\lambda x. (\lambda x. (\lambda x.x)))123$$ which is, with a leftmost bracketing convention, to be read as $$(((\lambda x. (\lambda x. (\lambda x. x)))1)2)3$$

In this term, the first redex is $$(\lambda x. (\lambda x. (\lambda x.x)))1$$ which beta-reduces to $$(\lambda x. (\lambda x.x))[1/x]$$ i.e. $1$ is substituted for each free occurence of $x$ in $(\lambda x. (\lambda x.x))$. Since $x$ is already by another $\lambda$-abstraction (in fact two), there is no free occurrence of $x$. Hence, nothing is substituted.

In general, new abstractions in some inner subterm "overwrite" abstractions in a further outwards term. The first two $\lambda x$'s do not effectively bind anything. Here is why.

So in the first reduction, $1$ is not substiuted into anywhere and just disappears. The same happens for the second $\lambda x$ abstraction, which is "overwritten" by the innermost one and hence does nothing to the term $2$. So we have

$$(((\lambda x. (\lambda x. (\lambda x. x)))1)2)3 \rhd_\beta ((\lambda x. (\lambda x. x))2)3 \rhd_\beta (\lambda x.x)3$$

Now we have just one redex left, and in the subterm $x$, $x$ is free to be substitued by $3$, so we end up with

$$(\lambda x.x)3 \rhd_\beta 3$$

That is, the result (the $\beta$-normal form) of your term is $3$, because only the innermost abstraction (which forms a redex with $3$) takes precedence in binding the variable $x$, and the outer two are empty abstractions, making the terms $1$ and $2$ disappear.