2
$\begingroup$

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

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

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.

$\endgroup$
  • $\begingroup$ so how did it change from (λf.λx.f(fx)) to λy.y+1 o.O $\endgroup$ – user2869231 Oct 14 '13 at 1:33
  • $\begingroup$ @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$. $\endgroup$ – Kirill Oct 14 '13 at 1:37
  • $\begingroup$ ok, so that explains why there's 2 of λy.y+1 then. Got it. Thanks :) $\endgroup$ – user2869231 Oct 14 '13 at 1:42

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.