# 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}\\_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. 😃