Chapter 3: Church Numerals: Increment
Church Numerals
The most important data in computer programs are integers.
Let's define natural integers.
0=λs.λz.z1=λs.λz.s(z)2=λs.λz.s(s(z))3=λs.λz.s(s(s(z)))⋮n=λs.λz.sn(z)
Why should we define integers like this? What does s and z mean here?
Let's take 2 for example to watch how church numerals could be converted back to normal ones. let s=λx.(x+1),z=0, then:
2sz======(λs.λz.s(s(z)))szs(s(z))s(s(0))s(0+1)1+12
It is clear now: s stands for successor and z stands for zero. It is built based on recursion. And yes, it is exactly how natural numbers are defined mathematically.
Successor
To get the successor of a church numeral, just simply wrap an s around it.
S=λn.λs.λz.(s(nsz))Sn=n+1
Proof:
Sn======(λn.λs.λz.(s(nsz)))(λs.λz.sn(z))(λs′.λz′.(s′((λs.λz.sn(z))s′z′)))(λs′.λz′.(s′(s′n(z′))))(λs′.λz′.(s′n+1(z′)))(λs.λz.(sn+1(z)))n+1
Addition
A Church numeral n is actually a recursion builder repeating a function for n times. Making use of this the addition operation of church numerals could be deduced.
add=λmn.(mSn)add mn=m+n
It reads as if "evaluating mth successor of n".
Proof:
add mn======(λmn.(mSn))mn(λs.λz.sm(z))S(λs.λz.sn(z))λz.Sm(z)(λs.λz.sn(z))Sm(λs.λz.sn(z))λs.λz.sm+n(z)m+n
Actually, there is a direct definition of addition.
add=λm.λn.λs.λz.ms(nsz)
It reads as if "evaluating mth successor of 'nth successor of 0'".
Proof is similar to indirect one.
Multiplication