lambda calculus evaluation I have a question about lambda calculus. I just read that it doesn't matter in which way expressions get evaluated.
So my question is: $(\lambda f.\lambda x.f(fx)) (\lambda y.y+1) 2$
so we can evaluate this expression like this:
$(\lambda f.\lambda x.f(fx)) (\lambda y.y+1) 2$
$(\lambda x.(λy.y+1)(\lambda y.y+1)x) 2$
$((\lambda y.y+1)(\lambda y.y+1)2)$
$(\lambda y.y+1)(2+1)$
$2+1+1$
but what if we start evaluation like this:
$(\lambda f.\lambda x.f(fx)) (\lambda y.y+1) 2$
$(\lambda f.\lambda x.f(fx)) (2+1)$ ???
So how can I continue evaluation now? I know there should be some rules not letting me to start evaluation like this but what is that?
 A: It is true that in the $\lambda$-calculus it doesn't matter in which way expressions get evaluated, provided that the evaluation ends in a normal form (i.e. in a term that cannot be reduced any further). This property is called uniqueness of the normal form and it is a consequence of confluence.
Your term does not contradict the uniqueness of the normal form. Indeed, in $(\lambda f. \lambda x.f(fx)) (\lambda y.y+1) 2$ there is only one $\beta$-redex, i.e. only one sub-term that can be reduced: $(\lambda f. \lambda x.f(fx)) (\lambda y.y+1)$. Thus, you can start only the first evaluation you wrote.
Why? If you have a term of the form $MNL$ then it has to be read as $(MN)L$, and you cannot read it as $M(NL)$. This is the unambiguous way terms are defined in the $\lambda$-calculus.
So, your term $(\lambda f. \lambda x.f(fx)) (\lambda y.y+1) 2$ is actually $\big( (\lambda f. \lambda x.f(fx)) (\lambda y.y+1) \big) 2$ and hence you cannot start the second evaluation you wrote. 

Note that there is the same mistake also at the end of your first evaluation: the term $(\lambda y.y+1)(\lambda y.y+1)2$ has to be read as $\big( (\lambda y.y+1)(\lambda y.y+1) \big) 2$ and not as $(\lambda y.y+1) \big((\lambda y.y+1)2\big)$, hence it $\beta$-reduces to  $(\lambda y.y+1+1) 2$ and not to $(\lambda y.y+1) (2+1)$.
