# beta reduction bascis

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

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

Can anyone explain where I'm going wrong?

## migrated from mathoverflow.netNov 12 '13 at 12:28

This question came from our site for professional mathematicians.

• 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$. – user43208 Nov 12 '13 at 12:27
• 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. – Andreas Blass Mar 15 '14 at 14:12

$$(\lambda x ~.~ xx)(\lambda z ~.~ zz) ~ \rightarrow_{\beta} ~ (xx)[x \mapsto (\lambda z ~.~ zz)] ~=~ (\lambda z ~.~ zz)(\lambda z ~.~ zz)$$
• 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. – portin.daniel Nov 12 '13 at 14:26