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.

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.
• It doesn't. You wrote $λmnfx.m(m\, f(n\, f\, x))$. There are multiple problems with that. First, your outermost expression inside the lambda is $m\, (\ldots)$ - but if anything, it should be $m\, (\ldots)\, x$. Second, watch what happens if $n \equiv N(0)$. You get $\lambda mnfx.m\, (m\, f(x))$, which doesn't look like it'll reduce to $N(0)$, no matter wheter you append that missing $x$ or not... – fgp Dec 7 '13 at 0:11
• One possible source of confusion may be that you need to be carefull with variable names when applying $\beta$-reductions. For example $(\lambda xy. (\lambda x.xy))z$ reduces to $\lambda y.(\lambda x.xy)$, not $\lambda xy.(\lambda x.zy)$. – fgp Dec 7 '13 at 0:21