Evaluation of $\beta$-reduction of $~\left(\lambda x ~.~x~x~x \right)\left(\lambda x ~.~x~x~x \right)\left(\lambda x ~.~x~x~x \right)$

Question

$$\begin{align} \Delta&:= \lambda x ~.~x~x~x\\ \Delta\Delta&\rightarrow_\beta\Delta\Delta\Delta\\ \left(\lambda x ~.~x~x~x \right) \left(\lambda x ~.~x~x~x \right)&\rightarrow_\beta \left(\lambda x ~.~x~x~x \right)\left(\lambda x ~.~x~x~x \right)\left(\lambda x ~.~x~x~x \right)\\ \end{align}$$

$$ \underbrace{\color{fuchsia}{\Delta\Delta\Delta\rightarrow_\beta\Delta\Delta\Delta\Delta}}_{\text{I want to derive this} } $$

$$\begin{align} \Delta\Delta\Delta= \color{red}{\left(\lambda x ~.~x~x~x \right)}\color{green}{\left(\lambda x ~.~x~x~x \right)}\color{blue}{\left(\lambda x ~.~x~x~x \right)} \end{align}$$

In the first place, I've been confused where should I start of application(=substitution?) in above colored lambda terms.

At least I can guess that in the first step, the red term can't be an argument of substitution.

So the possible patterns are as follows

1. plug $~ \color{blue}{\left(\lambda x ~.~x~x~x \right)} ~$ into $~ \color{green}{\left(\lambda x ~.~x~x~x \right)} ~$.

2. plug $~ \color{green}{\left(\lambda x ~.~x~x~x \right)} ~$ into $~ \color{red}{\left(\lambda x ~.~x~x~x \right)} ~$.

What is the correct order of $~ \beta$-reduction in this case?

Here I continue with the first option above.

$$\begin{align} \Delta\Delta\Delta&= \color{red}{\left(\lambda x ~.~x~x~x \right)}\color{green}{\left(\lambda x ~.~x~x~x \right)}\color{blue}{\left(\lambda x ~.~x~x~x \right)}\\&= (\Delta)(\Delta)(\Delta)\\ &= (\Delta) \underbrace{\left(\Delta\Delta\Delta \right)}_{ \color{blue}{\text{b}}~\text{to}~\color{green}{\text{g}} }\\&= \underbrace{\left( \lambda x ~.~x~x~x \right)\left(\left(\lambda x ~.~x~x~x \right)\left(\lambda x ~.~x~x~x \right)\left(\lambda x ~.~x~x~x \right) \right)}_{\text{An order problem arises again} } \\&= \left(\lambda x ~.~x~x~x \right) \left(\Delta\Delta\Delta \right)\\&= \left(\Delta\Delta\Delta \right)\left(\Delta\Delta\Delta \right)\left(\Delta\Delta\Delta \right)\\&\neq \Delta\Delta\Delta\Delta \end{align}$$

I need your help.

Answer 1

Parentheses are important in λ-calculus, because $(f g) h$ is different from $f (g h)$ in most cases. Usually parentheses are omitted, in which case one means the first of the two variants. (See e.g. Wikipedia) So the convention is to choose the second option which you listed.