lambda calculus reduction: (((lambda f (lambda x (f x))) (lambda y (* y y))) 12)

Question

given the input

(((lambda f (lambda x (f x))) (lambda y (* y y))) 12)

what does this step evaluate to: lambda x (f x)

I am trying to evaluate this and I have the following tree so far:

how do I evaluate this ? looking for guidance on what I might be doing wrong or how to proceed with this.

Answer 1

Lambda expressions are evaluated by reducing the leftmost redex first. A redex is something of the form $(\lambda a.b)c$ . Your expression is $(\lambda f.\lambda x.fx)(\lambda y . *yy)~12$. So your first redex is

$$(\lambda f.\lambda x.fx)(\lambda y . *yy)$$

So you substitute $(\lambda y . *yy)$ for $y$ in $\lambda x.fx$ to get $$\lambda x.(\lambda y . *yy)x~ 12$$

Then your next redex is the entire expression, ($(\lambda y . *yy)x$ is also a redex but it isn't the leftmost one) substituting $12$ in for $x$. So you get $$(\lambda y . *yy)~12$$

Then your last redex is the entire expression again so you get

$$*~12~12$$