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


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?

  • $\begingroup$ 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) $$ $\endgroup$ – 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)$.

  • 1
    $\begingroup$ 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. $\endgroup$ – Derek Elkins Jan 21 at 19:49
  • $\begingroup$ @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$. $\endgroup$ – Taroccoesbrocco Jan 21 at 20:00
  • $\begingroup$ What is the reason of the downvote? $\endgroup$ – Taroccoesbrocco Jan 22 at 3:21

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.