Beta reduction result

72 Views Asked by At

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!

1

There are 1 best solutions below

5
On BEST ANSWER

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*}$$