Church Numerals

Tags: mathsλ-calculus

This weekend I spent some time solving exercises of Introduction to Lambda Calculus. There is one notable exercise where I spent quite sometime figuring out the proof. It was:

Given Church numeral $|\textbf{c}_n \equiv \lambda f.\lambda x.f^n(x)|$, a lemma ($|(\textbf{c}_nx)^m (y) = x^{n*m}(y)|$), and a proposition $|\textbf{A}_* \equiv \lambda x.\lambda y.\lambda z.x(yz)|$, prove $| \textbf{A}_* \textbf{c}_n\textbf{c}_m = \textbf{c}_{n*m} |$ using the lemma.

Following is my proof for the same:

\begin{aligned} L.H.S. = \textbf{A}_*\textbf{c}_n\textbf{c}_m &= (\lambda xyz.x(yz)) \textbf{c}_m\textbf{c}_n & \\ &= \lambda z . \textbf{c}_m (\textbf{c}_n z) & \\ &= \lambda z . (\lambda f . \lambda y . f^m(y)) (\textbf{c}_n z) & [ \because \text{Church numeral } \textbf{c}_n \equiv \lambda f. \lambda x.f^n(x)] & \\ &= \lambda z . \lambda y . (\textbf{c}_n z)^m(y) & \\ &= \lambda z . \lambda y . z^{m*n} (y) & [ \because (\textbf{c}_nx)^m (y) = x^{n*m}(y) ] \\ &= \textbf{c}_{n*m} = R.H.S. \end{aligned}

Hence proved.

Most of the time was spent understanding the lemma, and figuring out difference in superscript value in the R.H.S. of $|\textbf{c}_n|$, w.r.t. in the R.H.S. of lemma. In $|\textbf{c}_n|$ it is the times, whereas in lemma it's exponent. It was fun. 😄