Motivation: Abstraction Level Up!

1. Apply square 3 times to 2

   1 ]=> (square (square (square 2)))
   
   ;Value: 256
   

2. 2 → x: Apply square 3 times to some number x, use lambda to abstract 2 to x

   (define square3 (lambda (x) (square (square (square x)))))
   

3. square → f: Apply some function f 3 times to some value x, similarly, use lambda to abstract square to f

   (define three_times_f (lambda (f x) (f (f (f x)))))
   

4. $3 → i$ : Apply some function f to value x for $i$ times $(i \in \mathbb{N})$

   • $i=0$

     (define zero_time_f (lambda (f x) (x)))
     

   • $i=1$

     (define one_time_f (lambda (f x) (f x)))
     

   • $i=2$

     (define two_times_f (lambda (f x) (f (f x))))
     

   • Recursive definition of $i$ applications

     • Base case:

       (define zero_time_f (lambda (f x) (x)))
       

     • Recursive step:

       (define (succ z) (lambda (f x) (f (z f x))))
       

     • Recursively solve for $i$ applications corresponding to $i$:

       (define (church i) 
           (if (= i 0)
               zero_time_f
               (succ (church (- i 1)))
           )
       )     
       

       This is the Church Encoding corresponding to natural number $i$.

       A simple test in REPL: Apply cube 2 times to 3 $((3^3)^3=19683)$

       1 ]=> (church 2)
       ;Value: #[compound-procedure 15]
       
       1 ]=> ( #[compound-procedure 15] cube 3)
       ;Value: 19683
       

Understanding Church Encoding

Church Encoding is NOT:

• Numbers that target to be stored in physical memory or represented in bits

• Designed for arithmetic operations (like $3.14 × 2.17$)

Church Encoding is:

• An abstraction of counting

Church Encoding is an abstraction of the counting process. In the context of Lambda Calculus, the three rules for inductively defining $λ-terms$ involve $atom$, $abstraction$, and $application$. Church Encoding can be understood as: given an initial $term$ and an $abstraction$, we want to apply this $abstraction$ to the $atom$ multiple times ($apply$). We use a higher-level $abstraction$ to abstract the process of counting these “multiple times”, and this layer of abstraction for the counting process is Church Encoding.

Church Encoding in Scheme

$zero：λf.λx.x$

Applying any $abstraction$ 0 times to a $term$ returns the original $term$.

(define zero (lambda (f x) x))

$one：λf.λx.(f x)$
$two：λf.λx.(f (f x))$
$three: λf.λx.(f (f (f x)))$

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

When writing thr, we notice the recursive structure. The base case is clearly zero, and the recursive step succ is as follows:

(define (succ z) (lambda (f x) (f (z f x))) )

Application Examples

Church Encoding is an abstraction of counting. If we want to square (square) the number 2 three times: $((2^2)^2)^2=256$

1 ]=> (thr square 2)
;Value: 256

Verify the correctness of succ:

1 ]=> (succ (succ (succ zero)))
;Value: #[compound-procedure 17]

1 ]=> (#[compound-procedure 17] square 2)
;Value: 256

References

• Church Encoding wiki

• Types and Programming Languages, Chapter 5 The Untyped Lambda-Calculus

• A Zhihu answer