I have trouble, when attempting to multiply Church numerals with lambda.
First, does this work?
MULT := $\lambda$mnfx.m ( PLUS n )
MULT := $\lambda$mnfx.m ( m SUCC n )
MULT := $\lambda$mnfx.m(m f(n f x))
Therefore if I multiply 3 ($\lambda$fx.f(f(f x))) and 4 ($\lambda$fx.f(f(f(f x)))), it should look like this when I start:
($\lambda$mnfx.m(m f(n f x)))($\lambda$fx.f(f(f x)))($\lambda$fx.f(f(f(f x))))
:= $\lambda$fx.$\lambda$fx.f(f(f x))($\lambda$fx.f(f(f x)) f($\lambda$fx.f(f(f(f x))) f x))
:= $\lambda$fx.$\lambda$fx.f(f(f x))($\lambda$fx.f(f(f x)) f(f(f(f(f x)))))
This is where I am confused. Do I do ($\lambda$fx.f(f(f x)))[f := f(f(f(f(f x))))]? Or ($\lambda$fx.f(f(f x)))[f := f][x := f(f(f(f x)))]?
If I do the first, then I end up with:
:= $\lambda$fx.$\lambda$fx.f(f(f x))($\lambda$fx.f(f(f x)) f(f(f(f(f x)))))
:= $\lambda$fx.$\lambda$fx.f(f(f x))($\lambda$x.f(f(f(f(f x))))(f(f(f(f(f x))))(f(f(f(f(f x)))) x))
And I am unsure of where to go from there, because I have no parameters for the x.
If I do the second, then I end up with:
:= $\lambda$fx.$\lambda$fx.f(f(f x))(f
:= $\lambda$fx.f(f(f(f(f(f(f(f(f x))))))))
or 3 * 4 = 8, so that cannot be right.
It seems that you're encoding the integer $n$ as $$ \textrm{N}(n) \equiv \lambda fx.\underbrace{f( \ldots f(f x) \ldots)}_{n\text{ applications}} $$
That makes multiplication easy - to multiply with $m$ you need to replace every $f$ with $m$ copies of $f$, and that's exactly what the representation of $m$ already does. So you can just set $$ \textrm{MULT} \equiv \lambda nmfx. n (m f) x = \lambda nmf.n (m f) $$ where the second equivalence stems from an $\eta$-conversion.
For $3\cdot 4$ you get $$\begin{eqnarray} \textrm{N}(3) &\equiv& \lambda fx.f(f(fx)) \\ \textrm{N}(4) &\equiv& \lambda gy.g(g(g(gy))) \\ \textrm{MULT}\, \textrm{N}(3)\, \textrm{N}(4) &\equiv& \left(\underline{\lambda nm}h. n (m h)\right)\, \left(\lambda fx.f(f(fx))\right)\, \left(\lambda gy.g(g(g(gy)))\right) \\ &\overset{\beta}{=}& \lambda h. \left(\lambda fx.f(f(fx))\right) \left(\left(\underline{\lambda g}y.g(g(g(gy)))\right) h\right)\, \, \\ &\overset{\beta}{=}& \lambda h. \left(\underline{\lambda f}x.f(f(fx))\right) \left(\lambda y.h(h(h(hy)))\right)\, \, \\ &\overset{\beta}{=}& \lambda h. \left(\lambda x.\left(\lambda y.h(h(h(hy)))\right)\left(\left(\lambda y.h(h(h(hy)))\right)\left(\left(\underline{\lambda y}.h(h(h(hy)))\right)x\right)\right)\right) \\ &\overset{\beta}{=}& \lambda h. \left(\lambda x.\left(\lambda y.h(h(h(hy)))\right)\left(\left(\underline{\lambda y}.h(h(h(hy)))\right)\left(h(h(h(hx)))\right)\right)\right) \\ &\overset{\beta}{=}& \lambda h. \left(\lambda x.\left(\underline{\lambda y}.h(h(h(hy)))\right)\left(h(h(h(h(h(h(h(hx)))))))\right)\right) \\ &\overset{\beta}{=}& \lambda h. \left(\lambda x.h(h(h(h(h(h(h(h(h(h(h(hx)))))))))))\right) \\ &=& \lambda hx.h(h(h(h(h(h(h(h(h(h(h(hx))))))))))) \\ &\equiv& \textrm{N}(12)\textrm{.} \end{eqnarray}$$ Equivalences marked with $\beta$ stem from $\beta$-reductions, and the reduced $\lambda$-expression is marked by underlining. The other equivalances are of syntatic nature.