# Brackets in Lambda Calculus with multiple lambdas

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?

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.