# How many possible Beta-reductions considering order of the expression $(\lambda x.\lambda y.y)(\lambda x.x) ((\lambda x.x) (\lambda y.y))$

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

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

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