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:

enter image description here

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?


1 Answer 1


$$ (\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))$$


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


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.