How to multiply in Lambda Calculus? 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.
 A: 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.
