snippetMinor
How do I arrive at the multiplication function in lambda calculus?
Viewed 0 times
arrivethemultiplicationcalculusfunctionhowlambda
Problem
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?
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?
Solution
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)
$$
Hence
$$ \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)$$
$$s ^ {(n \cdot m)} =
\left( s ^ {(m)} \right) ^ {(n)} =
\bar{n} \left(s ^ {(m)} \right) =
\bar{n}\ (\bar{m}\ s)
$$
Hence
$$ \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)$$
Context
StackExchange Computer Science Q#86990, answer score: 5
Revisions (0)
No revisions yet.