# evaluate the lambda expression call by value

$(\lambda x.\lambda y.(\lambda x.yx)xy)(\lambda y.y)(\lambda x.x(\lambda y.y))$

I know in $(\lambda x.M)N$, if M has bound variables same as free variables in N, we rename the bound variables. IN this problem I tried taking M as $\lambda y.(\lambda x.yx)xy$ and N as $(\lambda y.y)$. Here y is bound in both M and N do I need to rename.

Any simpler way to solve this?

-

Your starting expression presumes that shadowing variables bound in an outer scope is valid: in $\lambda y.(\lambda x.yx)xy$ the two $x$ variables are different.

Given that, substituting a closed term into another term will never require alpha conversion. In the resulting term $\lambda y.(\lambda x.yx)(\lambda y. y)y$ the two $y$ variables are distinct just as the $x$s were before.

Alpha conversion is just bureaucratic busywork, anyway. A bound variable is and always will be permanently tied to its binder; renaming is required only to prevent our notation from sabotaging that property.

-