I just started learning lambda calculus, and i have this question to do with normal order and in applicative order:
(λfx.f (f x))(λfx.f (f x)) f x
In normal order, I got the answer of (f (f (f (f x)))).
I tried applicative order like this:
-> (λfx.f (f x))(λfx.f (f x)) a b
-> (λfx.f (f x))(λx.a (a x)) b
-> (λfx.f (f x))(a (a b))
-> (λx.(a (a b)) ((a (a b)) x))
But I think this is wrong, so I asked the professor, and he gave me the "starting" portion of the solution, but I don't really understand it:
(λfx.f (f x))(λfx.f (f x)) f x
-> (λyx.y (y x))((λyx.y (y x)) f) x
-> (λyz.y (y z)) f ((λyz.y (y z)) f x) ;why is there an extra f?
My question is: why does the solution start off like this? Why does changing the variables add another $f$ in the middle?
Best Answer
Under normal order evaluation, an expression is evaluated by reducing the leftmost outermost $\beta$-redex first. So, in your example you get:
\begin{align} (\lambda fx.f (f x))(\lambda fx.f (f x)) f x &= \big(\lambda fx.f (f x)\big)(\lambda gy.g (g y)) f x \\ &\to \big(\lambda x. (\lambda gy.g (g y)) ((\lambda gy.g (g y)) x) \big) f x \\ &\to \big(\lambda gy.g (g y) \big) ((\lambda gy.g (g y)) f) x \\ &= \big(\lambda gy.g (g y) \big) ((\lambda gz.g (g z)) f) x \\ &\to \big(\lambda y. ((\lambda gz.g (g z)) f) ( ((\lambda gz.g (g z)) f) y) \big) x \\ &\to \big(\lambda gz.g (g z)\big) f ( ((\lambda gz.g (g z)) f) x) \\ &\to \big(\lambda z.f (f z)\big) ( ((\lambda gz.g (g z)) f) x) \\ &\to f (f ( ( \big(\lambda gz.g (g z) \big) f) x) ) \\ &\to f (f ( \big(\lambda z.f (f z) \big) x) ) \\ &\to f (f ( f (f x) ) ) \end{align}
According to applicative order evaluation, function's arguments are evaluated before the function is applied. In the $\lambda$-calculus, it means that you reduce the leftmost $\beta$-redex $(\lambda x. M)N$ provided that $N$ is a value, i.e. a variable or an abstraction.
\begin{align} (\lambda fx.f (f x))(\lambda fx.f (f x)) f x &= \big(\lambda fx.f (f x)\big)(\lambda gy.g (g y)) f x \\ &\to \big(\lambda x. (\lambda gy.g (g y)) ((\lambda gy.g (g y)) x) \big) f x \\ &\to (\lambda gy.g (g y) ) (\big(\lambda gy.g (g y)\big) f) x \\ &\to \big(\lambda gy.g (g y) \big) (\lambda y.f (f y)) x \\ &= \big(\lambda gy.g (g y) \big) (\lambda z.f (f z)) x \\ &\to \big(\lambda y. (\lambda z.f (f z)) ( (\lambda z.f (f z)) y) \big) x \\ &\to (\lambda z.f (f z) ) ( f (f x)) \end{align}
You can see the difference between the two evaluation orders after two $\beta$-steps, when you get the term $(\lambda gy.g (g y) ) ((\lambda gy.g (g y)) f) x $: this term has the form $(\lambda g. M_g) ((\lambda g.M_g) f) x $ with $M_g = \lambda y.g (g y)$, so the leftmost $\beta$-redex is $(\lambda g. M_g) ((\lambda g.M_g) f)$ where the argument $(\lambda g.M_g) f$ is not a value. So, the leftmost $\beta$-redex can be reduced under normal order evaluation, but not according to applicative order evaluation, for which you have first to reduce the argument to a value.
Note that the last term I wrote in the applicative order evaluation is stuck because the argument $f(fx)$ of the $\beta$-redex is not a value and then we cannot perform any further $\beta$-steps.
The fact that in this case normal order and applicative order evaluations yield different results is not surprising. Indeed, they yield the same result provided that the starting term is closed, and your starting term is not closed (the last occurrences of $f$ and $x$ are free).
Some definitions of applicative order are more lax and allows you to reduce the term $(\lambda z.f (f z) ) ( f (f x)) $ because the argument $f(fx)$ of the $\beta$-redex is fully evaluated, although it is not a value. So you will get \begin{align} (\lambda z.f (f z) ) ( f (f x)) \to f(f(f(fx))) \end{align} also under this extended sense of applicative order.