I'm familiar with how Church numerals are defined in the lambda calculus, i.e. as functions that take two arguments and apply the first argument $n$ times to the second.

Then I have the successor and addition functions, both of which I managed to derive and understand:

$$\begin{align} \mathrm{succ} &:= \lambda nsz.s (n s z) \\ (+) &:= \lambda nm.n\ succ\ m \\ \end{align} $$

But multiplication is where I'm stuck.

I understand that we can define a multiplication function $(*)$ by adding the number $m$ to $0$ exactly $n$ times. After all, $3 \times 2$ is simply $2 + 2 + 2 + 0$.

So that could mean that $(*)$ looks like this:

$$(*) := \lambda nm.n\ ((+)\ m)\ 0$$

This appears to be a somewhat intuitive definition of a lambda calculus multiplication function to me, and if I try it out with $2$ and $3$, after some messy reductions, the result seems correct and $(*)\,2\,3 \rightarrow 6$.

But then elsewhere I found this definition for multiplication:

$$\mathrm{mult} := \lambda xya.x (y a)$$

Now I don't see how you arrive at this function $\mathrm{mult}$. My definition $(*)$, which takes two arguments, seems intuitive enough to me. But his here, which takes two arguments, one for the $x$ and $y$ respectively, which are the numbers to be multiplied, and then a third one $a$, just seems impenetrable to me—and I cannot figure out why it works, or how you would derive it.

Can somebody help me understand the reasoning and derivation of this $\mathrm{mult}$ function?

  • 2
    $\begingroup$ If you left only the essence of your question, it would be much much better. I think you don't really need steps 1 - 3 and that computation in step 4. $\endgroup$ Commented Jan 19, 2018 at 18:40
  • $\begingroup$ Apologies. This was my very first question here, and I may indeed have been too verbose. I edited my initial question and shortened it significantly to focus on the essence of my problem. $\endgroup$ Commented Jan 19, 2018 at 20:15
  • 1
    $\begingroup$ I also find your own $(*)$ easier to understand. The same approach also works for exponentiation $exp =\lambda n m.\ n((*) m)$. (By the way, exponentiation can also be done with $\lambda ab.\ ba$ which is even more cryptic than $mult$ is. It can be "decrypted" in similar ways, though.) $\endgroup$
    – chi
    Commented Jan 19, 2018 at 20:33
  • $\begingroup$ You may want to check the Mikrokosmos interpreter for doing this complex reductions: mroman42.github.io/mikrokosmos $\endgroup$ Commented Sep 25, 2019 at 12:24

1 Answer 1


You know that $(\bar{n}\ s)$ corresponds to $s^{(n)}$, i.e. function $s$ applied $n$ times to its argument. You want to obtain a function that iterates some function $s$ exactly $n \cdot m$ times. From the above observations and some simple rules for the composition of functions we can immediately derive the body of $\textsf{mult}$:

$$s ^ {(n \cdot m)} = \left( s ^ {(m)} \right) ^ {(n)} = \bar{n} \left(s ^ {(m)} \right) = \bar{n}\ (\bar{m}\ s) $$


$$ \textsf{mult}\ :=\ \overbrace{\lambda n m.}^\text{ parameters}\underbrace{(\lambda sz.n\ (m\ s) z)}_{\text{Church numeral}}$$

or, if we $\eta$-contract, we get

$$ \textsf{mult}\ :=\ \lambda nms.n\ (m\ s)$$

  • $\begingroup$ I'm unfamiliar with the term "η-contract", could you elaborate on that? I seem to be missing how you get from $\lambda nm.(\lambda sz.n\ (m\ s)z)$ to $\lambda nms.n\ (m\ s)$. $\endgroup$ Commented Jan 19, 2018 at 18:58
  • 2
    $\begingroup$ Roughly, $f$ and $(\lambda x. f x)$ behave the same. You can find more on this here. $\endgroup$ Commented Jan 19, 2018 at 19:01

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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