Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

For computing $2+3$, the lambda calculus goes the following: $(\lambda sz.s(sz))(\lambda wyx.y(wyx))(\lambda uv.u(u(uv)))$

I am having a hard time substituing and reaching the final form of $(\lambda wyx.y((wy)x))((\lambda wyx.y((wy)x))(\lambda uv.u(u(uv))))$. Can anyone provide step-by-step procedure?

share|improve this question
did you forget to write the two $\lambda$ in front of $wyx.$ and of $uv.$ ? –  mercio Feb 24 '13 at 12:58
@mercio oops... –  UQT Feb 24 '13 at 13:05
add comment

1 Answer 1

up vote 1 down vote accepted

Recall that application is left-associative e.g. $w y x = \color{\red}{(}w y\color{red}{)} x$. Then the steps just follow by standard $\beta$-reduction and $\zeta_1$ (which reduces the left-hand side of an application, i.e. $e_1 \rightarrow e_1' \Rightarrow e_1 e_2 \rightarrow e_1' e_2$. In the following I have underlined the term which is about to be substituted:

$\color{red}{(}(\lambda sz.s(sz))\underline{(\lambda wyx.y(wyx))}\color{red}{)}(\lambda uv.u(u(uv)))$

$\xrightarrow{\zeta_1/\beta} (\lambda z.(λwyx.y(wyx))((\lambda wyx.y(wyx))z))\underline{(\lambda uv.u(u(uv)))}$

$\xrightarrow{\beta} (\lambda wyx.y(wyx))((\lambda wyx.y(wyx))(\lambda uv.u(u(uv))))$

Which is equal to your final form which has some additional parentheses to make clear the associativity of $w y z$ (i.e. $\lambda wyx.y((wy)x))((\lambda wyx.y((wy)x))(\lambda uv.u(u(uv))))$).

share|improve this answer
add comment

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.