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

Here is an expression that I am trying to reduce and my operations so far:

$$((\lambda x.(x (\lambda z.zy))) (\lambda z.\lambda y. zy) )= (x (\lambda z.zy))[x \to \lambda z.\lambda y. zy ] = ((\lambda z.\lambda y. zy) (\lambda z.zy)) = ((\lambda s.\lambda y. zy) (\lambda z.zy)) = \lambda y. zy$$

Is this procedure correct or am I making some small (or maybe big) mistake?

Thank you very much in advance for your comments.

share|cite|improve this question

$(\lambda z. \lambda y. zy) (\lambda z.zy)$
Before doing the $\beta$-reduction, $y$ is free in the term $\lambda z.zy$, while the name $y$ is bound inside the abstraction on the left, so we change that name on the left.
$(\lambda z. \lambda s. zs) (\lambda z.zy)$
Now we can do the $\beta$-reduction
$\lambda s. (\lambda z.zy) s$
Another $\beta$-reduction
$\lambda s. sy$

share|cite|improve this answer

My result is different:

(λz.λd.zd)(λz.zy) //rename z and y so capturing is avoided during substitution

I think you incorrectly renamed z to s.

share|cite|improve this answer
I don't think you are allowed to rename the free occurrence of $y$. – mercio Oct 9 '13 at 10:47
@mercio You are right I renamed wrong variable. I have corrected it. Result is the same anyway. – Trismegistos Oct 9 '13 at 11:31

Your Answer


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.