Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

$(\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?

share|improve this question

1 Answer 1

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.

share|improve this answer

Your Answer

 
discard

By posting your answer, you agree to the privacy policy and terms of service.

Not the answer you're looking for? Browse other questions tagged or ask your own question.