Church Numerals

Posted on

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}\\_n x)^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. 😃