Here is a lamba calculus expression:

$(\lambda x.\lambda y.y)(\lambda x.x)((\lambda x.x) (\lambda y.y))$

For simplicity let

$a:=(\lambda x.\lambda y.y)$

$b:=(\lambda x.x)$

$c:=(\lambda x.x)$

$d:=(\lambda y.y)$

Then I can re-write the expressions as evaluating $(a)(b)((c)(d))$, and I wish to compute how many different ways I can evaluate this expression using beta-reduction (which I am then supposed to write out). At first impulse I would think there would be $4!=24$ ways to do this by simply choosing all orderings of $a,b,c,d$ evaluations, but this seems like too many results ( now that I think about it I even see that it could be 5!). Any hints appreciated, there is something I am not understanding about the order of evaluations in Beta Reductions.

I also know that Beta-reductions are left associative, so the initial expression is equivalent to : $((\lambda x.\lambda y.y)(\lambda x.x))((\lambda x.x) (\lambda y.y))$

  • $\begingroup$ What does it mean $\lambda x.x. \lambda y.y$? Does It stand for $\lambda x. x(\lambda y.y)$? $\endgroup$ Nov 10, 2018 at 23:16
  • $\begingroup$ @Taroccoesbrocco typo, sorry. Modified to match the original question in my textbook. $\endgroup$ Nov 10, 2018 at 23:40

1 Answer 1


There are only three ways to evaluate this. The first step is either evaluating the $$(\lambda x. \lambda y. y)\lambda x. x$$ or the $$ (\lambda x. x)\lambda y. y$$In the first case, you can then choose to evaluate these two ways: $$((\lambda x. \lambda y. y)\lambda x. x)((\lambda x. x)\lambda y. y) \to_{\beta}(\lambda y. y)((\lambda x. x)\lambda y. y) \to_{\beta}((\lambda x. x)\lambda y. y) \to_{\beta} \lambda y. y$$ or $$((\lambda x. \lambda y. y)\lambda x. x)((\lambda x. x)\lambda y. y) \to_{\beta}(\lambda y. y)((\lambda x. x)\lambda y. y) \to_{\beta}((\lambda y. y)\lambda y. y) \to_{\beta} \lambda y. y$$ in the second case you only have one way to go, $$((\lambda x. \lambda y. y)\lambda x. x)((\lambda x. x)\lambda y. y) \to_{\beta} ((\lambda x. \lambda y. y)\lambda x. x)(\lambda y. y) \to_{\beta} (\lambda y. y)(\lambda y. y) \to_{\beta} \lambda y.y $$

  • $\begingroup$ Ok. I guess I just thought that within a certain bracket there are even more ways of changing the order. Also can you explain why (λx.λy.y)λx.x evaluates to (λy.y) ? $\endgroup$ Nov 11, 2018 at 1:11
  • $\begingroup$ Thanks a lot for your help by the way! $\endgroup$ Nov 11, 2018 at 1:11
  • 1
    $\begingroup$ @IntegrateThis It wasn't a typo (sorry I just finished studying my brain is fried a bit), you replace all free x's in λy.y with λx.x, which results in λy.y. $\endgroup$
    – SpooFwen
    Nov 11, 2018 at 1:17
  • 1
    $\begingroup$ I completely understand now THANK YOU! $\endgroup$ Nov 11, 2018 at 1:23

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .