Church Numerals

Once more we send thanks and love to Church. For we can extend this simple language, we can encode numerals. For $num \in \mathbb{N} \cup \{0\}$ we get $$ 0 = \lambda s .\ \lambda z .\ z$$ $$ 1 = \lambda s .\ \lambda z .\ s\ z$$ $$ 2 = \lambda s .\ \lambda z .\ s\ (s\ z)$$ $$ 3 = \lambda s .\ \lambda z .\ s\ (s\ (s\ z))$$ and so on. The $s$ argument is for successor, and $z$ is for zero. $0$ is defined the same as $false$. We can now define a successor function $$scc = \lambda n .\ \lambda s .\ \lambda z .\ s\ (n\ s\ z)$$ Note that $c\ s\ z$ is the body for any $c$ a church numeral. We can define plus $$plus = \lambda m .\ \lambda n .\ \lambda s .\ \lambda z .\ m\ s\ (n\ s\ z)$$ that is given some numeral $m$ we substitute the last $z$ in the body with the body of another church numeral $n$. We can define times as $$times = \lambda m .\ \lambda n .\ m\ (plus\ n)\ 0$$ here we substitute each $s$ in the body of $m$ with $plus\ n$. We can define a test for checking whether some numeral is zero $$isZero = \lambda m .\ m\ (\lambda x .\ false)\ true$$ we can unroll for $1$:

isZero 1 => (\lambda m . m (\lambda x . false) 0) 1 => 1 (\lambda x . false) 0 => (\lambda x . false) 0 => false

Subtraction is way more involved. We need two auxiliary functions to define a predecessor function: $$zz = pair\ 0\ 0$$ $$ss = \lambda p .\ pair\ (snd\ p)\ (plus\ 1\ (snd\ p))$$ $$prd = \lambda m .\ fst\ (m\ ss\ zz)$$ and now we can define subtraction $$minus = \lambda m .\ \lambda n .\ n\ prd\ m$$ we can even define an equal function $$equal = \lambda m .\ \lambda n .\ and\ (isZero\ (minus\ m\ n))\ (isZero\ (minus\ n\ m))$$

That is it. You can experiment here:

// bools let true = \ t . \ f . t; let false = \ t . \ f . f; let and = \ b . \ c . b c false; // pairs let pair = \ f . \ s . \ b . b f s; let fst = \ p . p true; let snd = \ p . p false; // church numerals let 0 = \ s . \ z . z; let 1 = \ s . \ z . s z; let 2 = \ s . \ z . s (s z); let 3 = \ s . \ z . s (s (s z)); // num operators let scc = \ n . \ s . \ z . s (n s z); let plus = \ m . \ n . \ s . \ z . m s (n s z); let times = \ m . \ n . m (plus n) 0; // num operators decs let zz = pair 0 0; let ss = \ p . pair (snd p) (plus 1 (snd p)); let prd = \ m . fst (m ss zz); let minus = \ m . \ n . n prd m; // tests let isZero = \ m . m (\ x . false) true; let equal = \ m . \ n . and (isZero (minus m n)) (isZero (minus n m)); let test = \ l . \ m . \ n . l m n; // more numerals - we need scc for these let 4 = scc 3; let 5 = scc 4; test (equal (times 3 2) (minus (plus 4 5) 3)) yes no

Translating structure

Let $N = \mathbb{N} \cup \{0\}$. Let $C_n$ be the set of possible church numerals. We can create a formal structure of $N$ and the operation +, that is $M_N = (N,+)$. Sure this is closed under operation: for all $n_1, n_2 \in N$ we have that $n_1 + n_2 \in N$. It is associative and has the neutral element $0$. Hence $M_N$ is a monoid. We have designed $plus$ so that $plus\ c\ 0 = plus\ 0\ c = c$ for any $c \in C_n$. $plus$ is associative. So $M_C = (C_n,plus)$ is a monoid. If we agree that we can represent infinite many church numerals (that is we agree that we have unlimited heap size or virtual memory or what ever a physical computer has as representation limit), we can quite easily define injective (one to one) maps between $N$ and $C_n$. That is direct maps, eg: $$f_C(2) = \lambda s .\ \lambda z .\ s\ (s\ z)$$ and $$f_N(\lambda s .\ \lambda z .\ s\ (s\ z)) = 2$$ these maps preserve the semantics of $+$ and $plus$, eg: $$f_C(1 + 1) = plus\ (\lambda s .\ \lambda z .\ s\ z)\ (...)$$ hence they are isomorphic. Thus $M_N$ and $M_C$ are monoid isomorphisms, that is the church representation with $plus$ is essentially the same as natural numbers with +. We can do the same trick with $times$ and $\cdot$. However we run into trouble with minus and $-$ since the "structure" $(N,-)$ is not closed under operation ($2 - 3 = -1 \not \in N$) and hence isn't a formal structure.