Church Numerals - implement one, two, and addition

Question

Given the following exercise:

Exercise 2.6

In case representing pairs as procedures wasn't mind-boggling enough, consider that, in a language that can manipulate procedures, we can get by without numbers (at least insofar as nonnegative integers are concerned) by implementing 0 and the operation of adding 1 as

(define zero (lambda (f) (lambda (x)
x)))
(define (add-1 n) (lambda (f)
(lambda (x) (f ((n f) x)))))

This representation is known as Church numerals, after its inventor, Alonzo Church, the logician who invented the calculus.

Define one and two directly (not in terms of zero and add-1). (Hint: Use substitution to evaluate (add-1 zero)). Give a direct definition of the addition procedure + (not in terms of repeated application of add-1).

I wrote this solution. I'm not 100% certain what the correct answer is, and I'm not sure the best way to check my solution so it's possible that I have made a mistake in my answer. Please let me know what you think.

;given definitions
(define zero (lambda (f) (lambda (x) x)))
(define (add-1 n)
 (lambda (f) (lambda (x) (f ((n f) x)))))
; exercise 2.6: define one and two directly -
; not in terms of zero or add-1
(define one
 (lambda (f) (lambda (x) (f (f x)))))
(define two
 (lambda (f) (lambda (x) (f ((f (f x)) x)))))
(define (church-plus a b)
 (define (church-num n)
 (cond ((= 0 a) (lambda (x) x))
 ((= 1 a) (lambda (f) (lambda (x) (f ((n f) x)))))
 (else (church-num (- n 1)))))
 (church-num (+ a b)))

• Val: I see that you can define 'inc' as function inc(n,f,x) {n(f(x))} and function inc(n,f,x) {f(n(x))}. Right?

Answer 1

Church defined numerals as the repeated application of a function. The first few numerals are defined thus:

(define zero (lambda (f) (lambda (x) x)))
(define one (lambda (f) (lambda (x) (f x))))
(define two (lambda (f) (lambda (x) (f (f x)))))

... and so on.

To see how one is derived, begin by defining one as (add-1 zero) and then perform the applications in order as shown in the steps below (I have written each function to be applied and its single argument on separate lines for clarity):

;; Givens
(define add-1 (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
(define zero (lambda (f) (lambda (x) x)))
(define one
 (add-1 ;; substitute with definition of add-1
 zero))
(define one
 ((lambda (n) ;; apply this function to argument zero
 (lambda (f) (lambda (x) (f ((n f) x)))))
 zero))
(define one
 (lambda (f) (lambda (x) (f ((zero ;; substitute with definition of zero
 f) x)))))
(define one
 (lambda (f) (lambda (x) (f (((lambda (f) ;; apply this function to argument f
 (lambda (x) x))
 f)
 x)))))
(define one
 (lambda (f) (lambda (x) (f ((lambda (x) ;; apply this function to argument x
 x)
 x)))))
(define one
 (lambda (f) (lambda (x) (f x)))) ;; we're done!

You may try your hand at two in a similar fashion. =)

By definition, Church numerals are the repeated application of a function. If this function were the integer increment function and the initial argument were 0, then we could generate all natural numbers 0, 1, 2, 3, .... This is an important insight.

Thus, a Church numeral is a function that takes one argument, the increment function, and returns a function that also takes one argument, the additive identity. Thus, if we were to apply a Church numeral to the integer increment function (lambda (n) (+ 1 n)) (or simply add1 in Scheme), which we then apply to the integer additive identity 0, we would get an integer equivalent to the Church numeral as a result. In code:

(define (church-numeral->int cn)
 ((cn add1) 0))

A few tests:

> (church-numeral->int zero)
0
> (church-numeral->int one)
1
> (church-numeral->int two)
2
> (church-numeral->int (add-1 two))
3
> (church-numeral->int (add-1 (add-1 two)))
4

A Church-numeral addition should take two Church numerals as input, and not integers, as in your code.

We use the insight above about increment functions and additive identities to notice that integer addition is simply repeated incrementing. If we wish to add integers a and b, we begin with the number b and increment it a times to get a + b.

The same applies to Church numerals. Instead of using integer increment function and integer additive identity, we use the Church increment function add-1 and we begin with a Church numeral as the additive identity. Thus, we can implement Church-numeral addition as:

(define (plus cn-a cn-b)
 ((cn-a add-1) cn-b))

A few examples:

(define three (plus one two))
(define four (plus two two))
(define five (plus two three))
(define eight (plus three five))

... and associated tests:

> (church-numeral->int three)
3
> (church-numeral->int four)
4
> (church-numeral->int five)
5
> (church-numeral->int eight)
8

• jaresty: How would you define plus without using add-1? I tried substitution but I'm finding it harder than I expected.
• Adeel Zafar Soomro: @jaresty: You don't need to avoid the use of add-1 in your definition of plus. You simply need to avoid its "repeated application." In other words, the definition of plus cannot be recursive.