arith.rkt

(define add (λ (n)
              (λ (m)
                (λ (f)
                  (λ (x)
                    ((n f) ((m f) x)))))))

(define mult (λ (n)
               (λ (m)
                 (λ (f)
                   (n (m f))))))

church-to-number.rkt

(define (church->number n)
  ((n add1) 0))

ones.rkt

; These two definitions of `one` are equivalent. Why?

(define one-manual (λ (f)
                     (λ (x)
                       (f x))))

(define one-computed (succ zero))

zero-and-succ.rkt

; zero is a function
(define zero (λ (f)
               (λ (x)
                 x)))

; succ ("successor") is also a function
(define succ (λ (n)
               (λ (f)
                 (λ (x)
                   (f ((n f) x))))))