2
$\begingroup$

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

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

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

$\endgroup$
  • $\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$ – IntegrateThis Nov 11 '18 at 1:11
  • $\begingroup$ Thanks a lot for your help by the way! $\endgroup$ – IntegrateThis Nov 11 '18 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 '18 at 1:17
  • 1
    $\begingroup$ I completely understand now THANK YOU! $\endgroup$ – IntegrateThis Nov 11 '18 at 1:23

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.