2

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!

MFranc
  • 213

1 Answers1

2

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

Luca Bressan
  • 6,845
  • 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? – MFranc Jul 16 '19 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})$$ – Luca Bressan Jul 16 '19 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). – Luca Bressan Jul 16 '19 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! – MFranc Jul 16 '19 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. – Luca Bressan Jul 16 '19 at 16:22