# 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?

• hey Amin, please use LaTeX or MathJax to edit your question.. Your question is not readable, thereby decreasing the probability of help. An example of a readable equation could be $$x^2 + 2x + 1 = f(x)$$ – Ahmad Bazzi Jan 9 at 13:03

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)$$.

• The order of evaluation does affect whether you reach a normal form or not. Two different evaluation order can't lead to two different normal forms, but one can fail to reach a normal form while the other succeeds. – Derek Elkins Jan 21 at 19:49
• @DerekElkins - You are right, thank you for the specification. I edited my answer. Anyway, note that by confluence whatever term $t$ is reached according to any evaluation starting from a term $t_0$, the unique normal form of $t_0$ can always be reached from $t$. – Taroccoesbrocco Jan 21 at 20:00
• What is the reason of the downvote? – Taroccoesbrocco Jan 22 at 3:21