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.

  • $\begingroup$ Thank you! I've been confused about this, and it really helps, but does my expression work as well? $\endgroup$ – Reed Oei Dec 6 '13 at 16:10
  • $\begingroup$ 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... $\endgroup$ – fgp Dec 7 '13 at 0:11
  • $\begingroup$ You don't define PLUS and SUCC, so it's kind of hard to guess what you actually mean to do there. Also, you seem to be having problems reducing the expression do get. Yet the lambda expressions in your question, quite frankly, make my eyes hurt way to much to wanna make me go through them and figure out exactly what your confusion may be. $\endgroup$ – fgp Dec 7 '13 at 0:16
  • 1
    $\begingroup$ 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)$. $\endgroup$ – fgp Dec 7 '13 at 0:21

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.