1

I am trying to reduce the following $\lambda$-expression: $$(\lambda x.x x) (\lambda y.y x) z$$ So I am reducing to $$(\lambda y.y x) (\lambda y.y x) z$$ That reduces to $$(\lambda y.y x)xz$$ Now comes trouble. According to the solution given here at letter k, you have: $$ (\lambda y.y x)xz \rightsquigarrow_\beta xxz$$ Bout from what I understand it should be: $$ (\lambda y.y x)xz \rightsquigarrow_\beta xzx$$ Because the lambda expression $(\lambda y.y x)$ just adds a final $x$ to the term that it is applied to.

What I am doing wrong?

Vitaly Olegovitch
  • 586

1 Answers1

5

As you said, the lambda expression $(\lambda y.yx)$ just adds a final $x$ to the term it's applied to. In the case at hand, it's applied to $x$, not to $xz$. Applying it to $x$ produces $xx$ while the $z$ at the end just sits there.

Remember the standard convention of lambda calculus that $abc$ means $(ab)c$, not $a(bc)$. That's why, in $(\lambda y.yx)xz$, the $(\lambda y.yx)$ is applied only to the $x$, not to the $xz$.

Andreas Blass
  • 71,833