lambda calculus beta reductions: ((((lambda f (lambda x ((f x) f))) (lambda y (lambda g (g (* y y))))) 2) (lambda a a))

My question is in continuation to lambda calculus reduction: (((lambda f (lambda x (f x))) (lambda y (* y y))) 12)

given the input:

((((lambda f (lambda x ((f x) f))) (lambda y (lambda g (g (* y y))))) 2) (lambda a a))


I want to understand the order of reductions that I should take. in the above mentioned question it was suggested to me to apply left most reduction.

I want to check if this is a valid 1st step towards leftmost reduction:

Or should f= λy.λg.g(*y y) instead ? What it might boil down to is: am I allowed to solve the sub-trees up before applying the solution from the right subtree on the left sub-tree?

$$(\lambda f. \lambda x .f x f) (\lambda y.\lambda g. g (* y y)) 2 (\lambda a. a)$$

The leftmost redex $$(\lambda a.b)c$$ is

$$(\lambda f. \lambda x .f x f)(\lambda y.\lambda g. g (* y y))$$

with

• $$a = f$$
• $$b = \lambda x .f x f$$
• $$c = (\lambda y.\lambda g. g (* y y))$$

Don't forget to make sure that $$x$$ doesn't exist in $$c$$, because if so then doing an immediate beta reduction would change the meaning of the expression. So the redex reduces to:

$$(\lambda x .(\lambda y.\lambda g. g (* y y)) x (\lambda y.\lambda g. g (* y y)))$$

Overall giving

$$(\lambda x . (\lambda y.\lambda g. g (* y y)) x (\lambda y.\lambda g. g (* y y))) 2 (\lambda a. a)$$

The next redex is $$(\lambda y. \cdots)x$$