在Church Numerals中构造前驱函数
Table of Contents
Church Numerals(丘奇数)
去年在皇帝新脑一书中学会了 Church Numerals , 设计非常精妙(与 Von Neumann 自然数的集合构造有异曲同工之妙), 是证明 λ-calculus 图灵完备的一个重要环节.
简单来说, Church Numerals 定义如下:
\[ \begin{array}{rcl}\textrm{ZERO} &:=&\lambda f. \lambda x. x \\\ \textbf{n} &:=&\lambda f. \lambda x. f^{(n)}(x)\end{array}\]
左侧加粗的 \(\textbf{n}\) 为 Church Numerals 中对应自然数 \(n\) 的项, 由此定义很容易写出后继函数(written in Scheme, 下同):
(define succ (lambda (n) (lambda (f) (lambda (x) (f ((n f) x))))))
有了 succ 函数, add , mul , pow 都可以层层推出:
(define (add n m) ((n succ) m)) (define (mul n m) (lambda (f) (lambda (x) ((n (m f)) x)))) (define (pow n m) (lambda (f) (lambda (x) (((m n) f) x))))
但是如何用 λ-calculus 表示减法? 我一开始的想法并不是在 Church Numerals 上做手脚, 而是像 \(\mathbb{N}\rightarrow \mathbb{Z}\) 那样变成两维, 用一个等价类 \(\{(x, x+n)\}\) 表示一个整数 \(n\) , 此时仍然可以依靠 succ 得出减法, 不过这个解决方案实在不优美.
前驱函数
直到今年做 PPCA 助教时, 我才重新了解了一下 Church Numerals 并发现了直接基于它的前驱函数 1。
Wiki 上的写法对于初学者非常不友好: \[ \textrm{PRED}:=\lambda n.\lambda f.\lambda x.n (\lambda g.\lambda h.h (g\textrm{ } f)) (\lambda u. x)(\lambda u.u)\]
一开始看到这个式子是完全懵逼的状态, 不过经测试运行得非常完美. 后来看了gregfjohnson和Church encoding的两份资料之后大致明白了 pred 的原理.
原理
求前驱也需要按照基本法, 由于 \(\textrm{PRED}(n) := {succ}^{(n-1)}(0)\) , 特别的, \(\textrm{PRED}(0) = 0\) .
由于 \(n-1\) 无法得到(事实上是我们的目标), 我们需要找一个函数 \(succ'\) 使得 \[{succ}^{(n-1)}(0) = {extract}\left({succ' }^{(n)}(c)\right)\] 其中 \(c\) 不依赖 \(n\) , \({extract}\) 用于最后的处理(也不依赖于 \(n\) ).
下面是几种构造方法, 前两种依赖于 pair (pair 及相关操作可以在 λ-calculus 中被构造出), 比较易懂, 最后一种则定义了一个与 Church Numerals 类似的结构:
构造 1
考虑 \(\{0, 0, 1, 2, 3, 4, 5, \cdots\}\) 这个数列, 它的第 \(n\) 项是 \(\textrm{PRED}(n)\) , 但是注意到 \(0\rightarrow0\) 与 \(0\rightarrow1\) 矛盾, 因此 \({succ'}\) 的自变量不能是一维.
(define c (make_pair 0 0)) (define succ' (lambda (p) (make_pair (second p) (succ (first p))))) (define extract (lambda (p) (first p)))
\(succ'\) 迭代作用过程: \((0,0)\rightarrow(0,1)\rightarrow(1,2)\rightarrow(2,3)\cdots\) .
构造 2
来自gregfjohnson, 将初始值区别对待, 加一个 \(\textit{true}\) 或者 \(\textit{false}\) 标签(if 条件表达式求值也可在 λ-calculus 中构造).
(define c (make_pair #t 0)) (define succ' (lambda (p) (if (first p) (make_pair #f (second p)) (make_pair #f (succ (second p)))))) (define extract (lambda (p) (second p)))
\(succ'\) 迭代作用过程: \((\textit{true},0)\rightarrow(\textit{false},0)\rightarrow(\textit{false},1)\rightarrow(\textit{false},2)\cdots\) .
构造 3
对于每个自然数 \(n\) , 定义 \[\mathcal{N} := \lambda h. \lambda f. \lambda x. h(f^{(n)}(x))\] 则可以得出 \[\begin{array}{rcl}{succ'} & = & \lambda \mathcal{N }. \lambda h. (h\textrm{ } (\mathcal{N}\textrm{ } f)) \\\ {extract} & = & \lambda \mathcal{N}.(\mathcal{N}\textrm{ } (\lambda u. u))\end{array}\] 但是 \(\mathcal{N}\) 与 Church Numerals 中的 \(\mathbf{n}\) 是同步的(对应于同一个自然数 \(n\) ), 因此我们需要 \(c\) 满足 \[({succ'} \textrm{ } c) = 0 = \lambda h.\lambda f.\lambda x. (h\textrm{ } x) \] 令 \(c\leftarrow \lambda u. x\) 正好满足.
将这些量带入: \[\textrm{PRED}:=\lambda n.\lambda f.\lambda x.{extract }(n\textrm{ }succ'\textrm{ } c)\] 中, 得出 \[ \textrm{PRED}:=\lambda n.\lambda f.\lambda x.n (\lambda g.\lambda h.h (g\textrm{ } f)) (\lambda u. x)(\lambda u.u)\]
Oh My Gawd: It's Full of Stars 2
有了 pred 之后, sub, leq 和 div 的构造顺理成章.
(define (sub n m) ((m pred) n)) (define (iszero? n) ((n (lambda (x) FALSE)) TRUE)) (define (leq n m) (iszero? (sub n m))) (define (div n m) ((leq m n) (succ (div (sub n m) m)) (ZERO)))
值得一提的是, 虽然可由对角线法则证明不存在可以判定两个函数是否等价的通用函数 equiv, 但是两个 Church Number 是否等价是可以判定的.
(define (equiv-church n m) (AND (leq n m) (leq m n)))
参考文献
- GregfJohnson, 构造 2, 入门资料.
- Church Encoding, wiki 上的资料.
- The emperor's new mind 皇帝新脑.