# Beta reduction result

I'm not understanding how to solve the following beta reduction :
$$(\lambda n.\lambda m.\lambda f.\lambda x.(n\,\,\,f)((m\,\,\,f)\,\,\,x))(\lambda f.\lambda x.ffffx)(\lambda f.\lambda x.fx)$$ My problem is with the notation, as far as I know an application has form (<func. exp> <args. exp>) and a function has form $$\lambda$$.<name><body>

I cant see any application where I can try to reduce.

I've tried considering $$(\lambda n.\lambda m.\lambda f.\lambda x.(n\,\,\,f)((m\,\,\,f)\,\,\,x))$$ and $$(\lambda f.\lambda x.ffffx)$$ as an application, resulting in :
$$\lambda m.\lambda f.\lambda x.(\lambda x.ffffx\,\,\,f)((m\,\,\,f)\,\,\,x))(\lambda f.\lambda x.fx) \implies \\ \lambda m.\lambda f.\lambda x.(\lambda x.ffffx)((m\,\,\,f)\,\,\,x))(\lambda f.\lambda x.fx) \implies \\ \lambda f.\lambda x.(\lambda x.ffffx)((\lambda f.\lambda x.fx\,\,\,f)\,\,\,x)) \implies \\ \lambda f.\lambda x.(\lambda x.ffffx)(\lambda x.fx\,\,\,x)) \implies \\ \lambda f.\lambda x.(\lambda x.ffffx)fx \implies \\ \lambda x.(\lambda x.fxfxfxfxx)$$ But it dosent really make sense to me...Any help in clarifying my mistakes is welcome!

You might want to use $$\alpha$$-conversion so that free variables don't end up being bound when they're supposed to remain free. Also, be careful with parentheses: $$\lambda x. M N$$ is not the same as $$(\lambda x. M) N$$.
In your case, I would apply $$\beta$$-reduction as follows:
\begin{align*} & (\color{blue}{\lambda n}. \lambda m. \lambda f. \lambda x. (\color{blue}n f)((m f) x))\color{red}{(\lambda f_1. \lambda x_1. f_1 f_1 f_1 f_1 x_1)}(\lambda f_2. \lambda x_2. f_2 x_2) \\ & \to_\beta (\lambda m. \lambda f. \lambda x. ((\color{blue}{\lambda f_1}. \lambda x_1. \color{blue}{f_1 f_1 f_1 f_1} x_1) \color{red}f)((m f) x))(\lambda f_2. \lambda x_2. f_2 x_2) \\ & \to_\beta (\lambda m. \lambda f. \lambda x. (\color{blue}{\lambda x_1}. f f f f \color{blue}{x_1})\color{red}{((m f) x))}(\lambda f_2. \lambda x_2. f_2 x_2) \\ & \to_\beta (\color{blue}{\lambda m}. \lambda f. \lambda x. f f f f ((\color{blue}m f) x))\color{red}{(\lambda f_2. \lambda x_2. f_2 x_2)} \\ & \to_\beta \lambda f. \lambda x. f f f f (((\color{blue}{\lambda f_2}. \lambda x_2. \color{blue}{f_2} x_2) \color{red}f) x) \\ & \to_\beta \lambda f. \lambda x. f f f f ((\color{blue}{\lambda x_2}. f \color{blue}{x_2}) \color{red}x) \\ & \to_\beta \lambda f. \lambda x. f f f f f x \end{align*}
• Thanks for your answer but one thing is still unclear to me. In step 4 how can you say that the correct step is to replace $\lambda$ m with $(\lambda f_2.\lambda x_2. f_2 x_2)$?How can you tell not to replace $\lambda$ m with ((m f)x) instead? Commented Jul 16, 2019 at 15:49
• Pay attention to the parentheses. The term is $$\color{blue}(\lambda m. \lambda f. \lambda x. f f f f ((m f) x)\color{blue})\color{red}(\lambda f_2. \lambda x_2. f_2 x_2\color{red})$$ and not $$\color{blue}(\lambda m. \lambda f. \lambda x. f f f f \color{blue})\color{red}((m f) x\color{red})\color{green}(\lambda f_2. \lambda x_2. f_2 x_2\color{green})$$ Commented Jul 16, 2019 at 15:57
• Also, since you are using Church encoding, you should expect each of the variables $n$ and $m$ to be substituted by a Church numeral (in this case, the $\lambda$-terms representing $4$ and $1$ respectively). Commented Jul 16, 2019 at 16:03
• Ok, but what about the last step? $$\lambda f.\lambda x.ffffx(fx)$$ Why is that not a substitution?I'd think the result is : $$\lambda x.fxfxfxfxx$$ But you just append the result to the function, how come?Thanks a lot by the way! Commented Jul 16, 2019 at 16:09
• First of all, there is an abuse of notation here, because application is left-associative (i.e., $L M N$ means $(L M) N$), but by writing $f f f f x$ we actually mean $f (f (f (f x)))$ (otherwise these terms would not be Church numerals). So yes, I shouldn't just append $f x$ at the end. Anyway, the term $\lambda f. \lambda x. f f f f x (f x)$ has no $\beta$-redex. Instead, the term $(\lambda f. \lambda x. f f f f x)(f x)$ reduces to $\lambda x_1. (f x) (f x) (f x) (f x) x_1$, where the bound $x$ is renamed through $\alpha$-conversion so that the free $x$ in $f x$ doesn't get bound. Commented Jul 16, 2019 at 16:22