Motivation: Abstraction Level Up!

1. 对 2 应用 $3$ 次 square

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

2. 2 → x: 对某个数 x 应用 $3$ 次 square，用 lambda 把 2 抽象到 x

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

3. square → f: 对某个值 x 应用 $3$ 次某个函数 f，类似地，用 lambda 把 square 抽象到 f

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

4. $3 → i$ : 对某个值 x 应用 $i$ 次某个函数 f $(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))))
     

   • 递归定义 $i$ 次应用

     • 递归基：

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

     • 递归步：

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

     • 递归求解 $i$ 对应的 $i$ 次应用：

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

       这就是自然数 $i$ 对应的 Church Encoding.

       在 REPL 中简单做一个测试：对 3 应用 $2$ 次 cube $((3^3)^3=19683)$

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

理解 Church Encoding

Church Encoding 不是：

• 可以被存储在物理存储器中的，可以用 bit 表示的数字

• 为了算数运算（类似 $3.14 × 2.17$ ）而设计

Church Encoding 是：

• 对 " 计数 " 的抽象

Church Encoding 是对计数过程的一种抽象，在 Lambda Calculus 的语境里，归纳定义 $λ-term$ 的三条规则分别涉及了 $atom$, $abstraction$, $application$，Church Encoding 可以理解为：有一个起始的 $atom$ 和一个 $abstraction$ ，我们希望对这个 $term$ 进行若干次 $abstraction$ 的应用（$apply$），我们使用更高一层的 $abstraction$ 来抽象对 " 若干次 " 进行计数的过程，这一层对于计数过程的抽象就是 Church Encoding.

Church Encoding in Scheme

$zero：λf.λx.x$

对某个 $term$ 进行 $0$ 次任意 $abstraction$ 的应用，返回值依然是原来的 $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)))))

写到 thr 的时候注意到这里的递归结构，递归基毫无疑问是 zero，递归步 succ 如下：

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

应用举例

Church Encoding 是对计数的抽象，如果我们希望对 2 进行 3 次平方（square）操作： $((2^2)^2)^2=256$

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

验证 succ 的正确性：

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

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

参考资料

• Church Encoding wiki

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

• 一则知乎回答