Could you please help me understand $\beta$ reductions' evaluation order. I've seen the most common approaches are
- Applicative : reduce the leftmost, innermost $\beta$ redex first.
- Normal : reduce the leftmost, outermost $\beta$ redex first.
- Unspecified : evaluate whatever you want but realize that there might be some order that doesn't terminate.
Now please indicate me if the following reductions are correct, according to each of the possible reductions order.
$$
(\lambda x.x((\lambda y.y)x))((\lambda a.a)(\lambda b.b))
$$
Normal :
$$
(\color{red}\lambda \color{red}x\color{red}.\color{red}x((\lambda y.y)\color{red}x))\color{blue}{((\lambda a.a)(\lambda b.b))} \equiv_{\beta} \\
((\color{red}{(\lambda a.a)}\color{blue}{(\lambda b.b)})((\lambda y.y)((\lambda a.a)(\lambda b.b)))) \equiv_{\beta} \\
(\color{red}{(\lambda b.b)}\color{blue}{((\lambda y.y)((\lambda a.a)(\lambda b.b)))}) \equiv_{\beta} \\
(\color{red}{(\lambda y.y)}\color{blue}{((\lambda a.a)(\lambda b.b))}) \equiv_{\beta} \\
(\color{red}{(\lambda a.a)}\color{blue}{(\lambda b.b)}) \equiv_{\beta} \\
(\lambda b.b)
$$
Applicative :
$$
(\lambda x.x(\color{red}{(\lambda y.y)}\color{blue}x))((\lambda a.a)(\lambda b.b)) \equiv_{\beta} \\
(\lambda x.xx)((\lambda a.a)(\lambda b.b)) \equiv_{\beta}
$$
$$
\text{here, do we consider the result } (\lambda x.x(x)) \text{ as an application of }\\
\\ \lambda x.x \text{ to } (x) \text{ ,with the necessary renaming of (x), or just as part of the body as in } \lambda x.xx
$$
$$
\color{red}{(\lambda x.xx)}\color{blue}{((\lambda a.a)(\lambda b.b))} \equiv_{\beta} \\
(\color{red}{(\lambda a.a)}\color{blue}{(\lambda b.b)})((\lambda a.a)(\lambda b.b)) \equiv_{\beta} \\
\color{red}{(\lambda b.b)}\color{blue}{((\lambda a.a)(\lambda b.b))} \equiv_{\beta} \\
(\color{red}{(\lambda a.a)}\color{blue}{(\lambda b.b)}) \equiv_{\beta} \\
(\lambda b.b)
$$
"Unspecified" :
$$
(\lambda x.x((\lambda y.y)x))(\color{red}{(\lambda a.a)}\color{blue}{(\lambda b.b)}) \equiv_{\beta} \\
(\color{red}{\lambda x.x}((\lambda y.y)\color{red}x))\color{blue}{((\lambda b.b))} \equiv_{\beta} \\
\color{red}{(\lambda b.b)}\color{blue}{((\lambda y.y)(\lambda b.b))} \equiv_{\beta} \\
\color{red}{(\lambda y.y)}\color{blue}{(\lambda b.b)} \equiv_{\beta} \\
(\lambda b.b)
$$
I guess this is an unfortunate case since, no matter the reduction order, the result is always the identity function (unless mistake were made!).
Best Answer
Your reduction sequences according to the normal order and the unspecified order are correct, but your second reduction sequence does not follow the applicative order. In order to understand why, some definitions are required.
A redex is a term of the form $(\lambda x M)N$. An outermost redex is a redex that is not contained inside another one. An innermost redex is one that has no redexes inside it (see here).
In your attempt to follow the applicative order (i.e. reducing the leftmost innermost redex), your first reduction step is correct. Now, consider $(\lambda x.xx)((\lambda a.a)(\lambda b.b))$: its leftmost innermost redex is $\color{red}{(\lambda a.a)}\color{blue}{(\lambda b.b)}$, and not $\color{red}{(\lambda x.xx)}\color{blue}{((\lambda a.a)(\lambda b.b))}$ because the latter contain a redex $\color{blue}{(\lambda a.a)(\lambda b.b)}$. Therefore, the correct reduction sequence following the applicative order is: \begin{align} &(\lambda x.x(\color{red}{(\lambda y.y)}\color{blue}x))((\lambda a.a)(\lambda b.b)) \\ \equiv_{\beta} \ & (\lambda x.xx)(\color{red}{(\lambda a.a)}\color{blue}{(\lambda b.b))} \\ \equiv_\beta \ & \color{red}{(\lambda x. xx)}\color{blue}{(\lambda b.b)} \\ \equiv_\beta \ & \color{red}{(\lambda b. b)}\color{blue}{(\lambda b.b)} \\ \equiv_\beta \ & \lambda b.b \end{align}
To see that the normal order reduces to a normal form while the applicative order diverges, consider the term $M = (\lambda y. x)(\delta\delta)$ where $\delta = \lambda z.zz$. Indeed, the leftmost outermost redex in $M$ is the whole term, which reduces to $x$; while the leftmost innermost redex in $M$ is $\delta\delta$, which reduces to itself.