Lambda Calculus Reduction
Applicative order: The leftmost, innermost redex is always reduced first.

Normal order: The leftmost, outermost redex is always reduced first.


Applicative order: $(λx.((λy.(∗2y))(+xy)))y$, the leftmost innermost redex is $(λy.(∗2y))(+xy)$. It is reduced first. Then we get $(λx.(∗2(+xy)))y$. Here $y$ is a free variable, renaming is not needed. Then the result is $(∗2(+yy))$.

Normal order:  $(λx.((λy.(∗2y))(+xy)))y \rightarrow ((λy.(∗2y))(+yy)) \rightarrow *2(+yy)$.
Applicative order: $$\begin{align*}(λx.λy.(xy))(λz.(zy)) &amp;\rightarrow_\alpha (λx.λw.(xw))(λz.(zy))\\ &amp;\rightarrow_{\phantom{\alpha}} λw.((λz.(zy))w) \\ &amp;\rightarrow_{\phantom{\alpha}} λw.wy\end{align*}$$
The first $y$ is bound, the second $y$ is free. When $x$ is substituted by $(λz.(zy))$, name capture occurs, so the bound y is renamed by $w$.

Normal order reduction is same as the applicative order.