0
$\begingroup$

Hi I get the basics of beta reduction e.g.

$$(\lambda var.body)arg $$

you just replace the occurrences of var with arg in body.

However what happens here?

$$(\lambda x.xx)(\lambda x.xx) \rightsquigarrow_\beta (\lambda x.xx)(\lambda x.xx)$$

Let's call them $A$ and $B$, so I replace all occurrences of $x$ in $A$ with $xx$ (from $b$) and throw away $B$'s lamda. Giving me

$$(\lambda x.xx)(\lambda x.xx) \rightsquigarrow_\beta \lambda x.xxxx$$

Instead of

$$ (\lambda x.xx)(\lambda x.xx)$$

Can anyone explain where I'm going wrong?

$\endgroup$

migrated from mathoverflow.net Nov 12 '13 at 12:28

This question came from our site for professional mathematicians.

  • $\begingroup$ MathOverflow is for mathematicians to ask questions of each other about their research, so this belongs elsewhere. I will migrate it to Mathematics StackExchange. But in brief, you need to substitute $\lambda x. xx$ for $x$, not $xx$. $\endgroup$ – user43208 Nov 12 '13 at 12:27
  • $\begingroup$ Where you're going wrong is "and throw away $B$'s lambda." The definition of beta reduction does not say to throw away $B$'s lambda; keep it, and you'll get the right answer. $\endgroup$ – Andreas Blass Mar 15 '14 at 14:12
2
$\begingroup$

$$ (\lambda x ~.~ xx)(\lambda z ~.~ zz) ~ \rightarrow_{\beta} ~ (xx)[x \mapsto (\lambda z ~.~ zz)] ~=~ (\lambda z ~.~ zz)(\lambda z ~.~ zz) $$

$\endgroup$
  • $\begingroup$ Hi i was told the answer was the same as the input i.e. (\x.xx)(\x.xx) $\endgroup$ – user2942720 Nov 12 '13 at 14:13
  • $\begingroup$ user2942720, $(\lambda x ~.~ xx)$ is $\alpha$-equivalent to $(\lambda z ~.~ zz)$. In general, you can arbitrarily rename variables bound by a $\lambda$-abstraction. The two terms are considered equivalent as $\lambda$-terms. $\endgroup$ – portin.daniel Nov 12 '13 at 14:26

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.