0
$\begingroup$

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?

$\endgroup$
3
$\begingroup$

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

$\endgroup$

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.