2

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

user2869231
  • 135

1 Answers1

2

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.

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