# Lambda Calculus: Reducing to Normal Form

I'm having trouble understanding how to reduce lambda terms to normal form. We just got assigned a sheet with a few problems to reduce, and the only helpful thing I've found is the following example in the book:

(λf.λx.f(fx))(λy.y+1)2

->(λx.(λy.y+1)((λy.y+1)x))2 //How'd it get to this??

->(λx.(λy.y+1)(x+1))2

->(λx.(x+1+1))2

->(2+1+1)

I'm pretty sure I understand most of it... except for their first step (everything else is pretty much substitution as if it was: f(x) = x + 3, x = y, therefore y+3)

Can someone please explain this to me? I pretty much have no experience with lambda calculus.

Thanks,

Sean

• apparently the z's in the original equation were x's... don't know how I managed that.. but question remains – user2869231 Oct 14 '13 at 1:24

Basically, the function $(\lambda f.\lambda x.f(fx))$ is applied to the argument $\lambda y.y+1$. This step is also called beta reduction.
• @user2869231 $\lambda f.\lambda x.f(fx)$ is a function that got applied to $\lambda y.y+1$; when that happened all occurrences of $f$ in $\lambda x.f(fx)$ were replaced with the expression $\lambda y.y+1$. – Kirill Oct 14 '13 at 1:37