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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.