I'm having difficulties understanding lambda calculus, specially identifying what's a redex. Which redexes are there in $\lambda s. \lambda z. (\lambda u. z)(\lambda v. v)$?

The book uses $(\lambda u. z) [u \to (\lambda v. v)]$,

but isn't $(\lambda s. \lambda z. (\lambda u. z))[s \to (\lambda v. v)]$ valid too?


1 Answer 1


You must learn how to put in parentheses and then it will be easier to figure out what is what. In the above case, we first put in parentheses: $$\lambda s . (\lambda z . ((\lambda u. z) (\lambda v . v))).$$ This is the only correct way to put back parentheses. For instance, this is wrong $$(\lambda s . (\lambda z . (\lambda u . z))) (\lambda v . v)$$ Why is it wrong? Because the rules for writing expressions without parentheses say that when you see $\lambda x . \cdots$ that means that $\lambda x$ binds the whole expression. For instance $\lambda x . x (\lambda y . y)$ is the same as $\lambda x . (x (\lambda y . y))$ and is diffrerent from $(\lambda x . x) (\lambda y . y)$.

If this is not resolving your dilemma you have to explain why you think that the other redex is valid.

  • $\begingroup$ Thanks, that helps a lot! Quick question: when I apply a parameter to a function, should I insert it parenthesized? Say I have $\text{f}=\lambda n. \lambda s. \lambda z. n (\lambda g. \lambda h. h (g s))$, and I want to evaluate $\text{f} c_0$, with $c_0=\lambda a. \lambda b. b$. Does it become $\lambda s. \lambda z. \lambda a. \lambda b. b (\lambda g. \lambda h. h (g s))$ or $\lambda s. \lambda z. (\lambda a. \lambda b. b) (\lambda g. \lambda h. h (g s))$? $\endgroup$
    – Clash
    Sep 7, 2013 at 12:37
  • $\begingroup$ You should parenthesize everything in sight until the day when you understand which things need not be parenthesized. $\endgroup$ Sep 9, 2013 at 14:38
  • $\begingroup$ Yes, I'm inserting parenthesis everywhere now, but could you please answer the question on the previous comment? It does make a difference to parenthesize the parameter in that case, doesn't it? $\endgroup$
    – Clash
    Sep 9, 2013 at 17:04
  • $\begingroup$ Yes, you should patenthesize the argument, unless it is a single letter or already paranthesized. $\endgroup$ Sep 9, 2013 at 20:31
  • $\begingroup$ Alright, so I think I got lambda calculus now... thanks so much for the help! If you'd be so kind, I even tried to answer a question that I think someone answered it wrong, could you take a quick glance? cs.stackexchange.com/questions/12740/… $\endgroup$
    – Clash
    Sep 10, 2013 at 5:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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