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