0
$\begingroup$

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?

$\endgroup$
1
$\begingroup$

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.

$\endgroup$
  • $\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 '13 at 12:37
  • $\begingroup$ You should parenthesize everything in sight until the day when you understand which things need not be parenthesized. $\endgroup$ – Andrej Bauer Sep 9 '13 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 '13 at 17:04
  • $\begingroup$ Yes, you should patenthesize the argument, unless it is a single letter or already paranthesized. $\endgroup$ – Andrej Bauer Sep 9 '13 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 '13 at 5:43

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

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