Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. Join them; it only takes a minute:

Sign up
Here's how it works:
  1. Anybody can ask a question
  2. Anybody can answer
  3. The best answers are voted up and rise to the top

$(\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|cite|improve this question

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