2
$\begingroup$

I wanted to show:

$$ (\lambda x . (\lambda y.x))yx \equiv_{\beta} y $$

the definition of beta equivalence is on page 17 of these notes.

I did a few attempts but got different things like $x$. I think my main confusion is how to interpret:

$$ yx $$

at the end. Does that mean we are applying $x$ to $y$ or that we are applying $yx$ to the lambda function $(\lambda x . (\lambda y.x))$? I tried both interpretations and didn't get anything that made sense.

I think I understand what $\beta$ conversion means (cuz I could follow the example he gave) but then when I tried doing it myself on this weird example I got non-sense.

$\endgroup$
5
$\begingroup$

I will make my answer more sophisticated by using parentheses. The first thing to realize is that $(\lambda x . (\lambda y . x)) y x$ is the same thing as $((\lambda x . (\lambda y . x)) y) x$ because in $\lambda$-calculus application associates to the left, which means that $A B C = (A B) C$. As you can see, $x y$ does not even appear in your expression.

After that, I would follow Yuval's observation that it is impolite to use the same variable for two different purposes: the $x$ and $y$ inside $\lambda$'s are not the same as the outer $x$ and $y$. We should rename bound variables to get $$((\lambda a . (\lambda b . a)) y) x$$ Can you do it from here?

P.S. Please stop pelting us with questions about $\lambda$-calculus that all look alike. Take them one at a time, wait for the answers, and think about them. It is likely subsequent questions will become redundant.

$\endgroup$
2
$\begingroup$

Here is an unsophisticated answer; undoubtedly more sophisticated ones will pop out in due time.

Let's change the leftmost $y$ to a $z$, to avoid confusion.

When you apply $\lambda x. (\lambda z.x)$ to $y$, you get $\lambda z.y$. When you apply this to $x$ (indeed, to anything at all), you get $y$.

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