# Which redexes are there in $\lambda s. \lambda z. (\lambda u. z)(\lambda v. v)$? How to substitute arguments?

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?

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)$.
• 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))$? – Clash Sep 7 '13 at 12:37