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

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.

• The tree is inconsistent. There are no "apply" nodes under "lambda" nodes. However, f is applied on x and (*) is applied on y and the result is again applied on y. Mar 23 '20 at 19:41
• The tree written is correct. Apply is just implicit in lambda calculus, indicated by concatenation. Mar 24 '20 at 0:16

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$$

• the leftmost redex concept is a little hard for me. What if the redex thats we are substituting is more complex that the one in this case, can we simplify it before substituting ? For E.g. (lambda y (lambda g (g (* y y)))) Mar 24 '20 at 4:14
• @Dhruv The expression you wrote there isn't a redex, I'll assume you mean it as the $c$ for some $(\lambda a.b)c$ . And the answer is...sometimes. Evaluating left to right gives you the property that if the lambda expression has a redex-free final form, then you will reach it. If you evaluate in arbitrary order, you could loop forever. Mar 24 '20 at 6:45
• I posted another question to cs.stackexchange.com/questions/122115/… as a follow up. Mar 25 '20 at 2:39