邱奇数

邱奇编码是把数据和运算符嵌入到lambda演算内的一种方式，最常见的形式即邱奇数，它使用lambda符号表示自然数。方法得名于阿隆佐·邱奇，他首先以这种方法把数据编码到lambda演算中。

透過邱奇編碼，在其他符号系统中通常被认定为基本的项（比如整数、布尔值、有序对、列表和tagged unions）都會被映射到高阶函数。在無型別lambda演算，函數是唯一的原始型別。

邱奇編碼本身並非用來實踐原始型別，而是透過它來展現我們不須額外原始型別即可表達計算。

很多学数学的学生熟悉可计算函数集合的哥德尔编号；邱奇编码是定义在lambda抽象而不是自然数上的等价运算。

邱奇数

邱奇数為使用邱奇编码的自然数表示法，而用以表示自然数$n$的高阶函数是個任意函数$f$映射到它自身的n重函数复合之函数，簡言之，數的「值」即等價於參數被函數包裹的次數。

$f^{\circ n}=\underset{n\text{ 次}}{\underbrace{f\circ f\circ \cdots \circ f}}.$

不論邱奇數為何，其都是接受兩個參數的函數。

$\begin{array}{ccc}\text{ 自 然 數}& \text{函 數 定 義}& \text{lambda 表 達 式}\\ 0& 0fx=x& 0=\lambda f.\lambda x.x\\ 1& 1fx=fx& 1=\lambda f.\lambda x.fx\\ 2& 2fx=f(fx)& 2=\lambda f.\lambda x.f(fx)\\ 3& 3fx=f(f(fx))& 3=\lambda f.\lambda x.f(f(fx))\\ ⋮& ⋮& ⋮\\ n& nfx=f^{n}x& n=\lambda f.\lambda x.f^{\circ n}x\end{array}$

就是说，自然数$n$被表示为邱奇数n，它对于任何lambda-项F和X有着性质：

n F X =_β Fn X。

使用邱奇数的计算

在 lambda 演算中，数值函数被表示为在邱奇数上的相应函数。这些函数在大多数函数式语言中可以通过 lambda 项的直接变换来实现（服从于类型约束）。

加法函数 $\text{plus}(m,n)=m+n$ 利用了恒等式 $f^{(m+n)}(x)=f^m(f^n(x))$。

plus ≡ λm.λn.λf.λx. m f (n f x)

后继函数 $\text{succ}(n)=n+1$ β-等价于（plus 1）。

succ ≡ λn.λf.λx. f (n f x)

乘法函数 $\text{times}(m,n)=m\times n$ 利用了恒等式 $f^{(m\times n)}=(f^m{)}^n$。

mult ≡ λm.λn.λf. n (m f)

指数函数 $\exp (m,n)=m^n$ 由邱奇数定义直接给出。

exp ≡ λm.λn. n m

前驱函数 $\text{pred}(n)=\{\begin{array}{cc}0& \text{if }n=0,\\ n-1& \text{otherwise}\end{array}$ 通过生成每次都应用它们的参数 g 于 f 的 $n$ 重函数复合来工作；基础情况丢弃它的 f 复本并返回 x。

pred ≡ λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)

邱奇數函數一表

函數	代數	等同	函數定義	Lambda 表達式
後繼	$n+1$	$f^{n+1}x=f(f^{n}x)$	$\mathrm{succ}nfx=f(nfx)$	$\lambda n.\lambda f.\lambda x.f(nfx)$	...
加法	$m+n$	$f^{m+n}x=f^m(f^{n}x)$	$\mathrm{plus}mnfx=mf(nfx)$	$\lambda m.\lambda n.\lambda f.\lambda x.mf(nfx)$	$\lambda m.\lambda n.n\mathrm{succ}m$
乘法	$m\times n$	$f^{m\times n}x=(f^m{)}^{n}x$	$\mathrm{multiply}mnfx=m(nf)x$	$\lambda m.\lambda n.\lambda f.\lambda x.m(nf)x$	$\lambda m.\lambda n.\lambda f.m(nf)$
指數	$m^n$	$nmf=m^{n}f$	$\exp mnfx=(nm)fx$	$\lambda m.\lambda n.\lambda f.\lambda x.(nm)fx$	$\lambda m.\lambda n.nm$
前驅*	$n-1$	${\mathrm{inc}}^n\mathrm{con}=\mathrm{val}(f^{n-1}x)$	$if(n==0)0else(n-1)$	$\lambda n.\lambda f.\lambda x.n(\lambda g.\lambda h.h(gf))(\lambda u.x)(\lambda u.u)$
減法*	$m-n$	$f^{m-n}x=(f^{-1}{)}^n(f^{m}x)$	$\mathrm{minus}mn=(n\mathrm{pred})m$	...	$\lambda m.\lambda n.n\mathrm{pred}m$

* 注意在邱奇編碼中,

• $\mathrm{pred}(0)=0$
• $m<n\to m-n=0$

除法函式

以下列定義可實作自然數的除法

$n/m=\mathrm{if}n\ge m\mathrm{then}1+(n-m)/m\mathrm{else}0$

計算 $n$ 除以 $m$ 的遞迴相減時，將會計算很多次的beta歸約。除非以紙筆手工來做，那麼多步驟倒無關緊要，
但我們不想一直重複瑣碎的歸約；而判別數字是否為零的函式是 IsZero，所以考慮下列條件：

$\mathrm{IsZero}(\mathrm{minus}nm)$

這個判別式相當於 $n$ 小於等於 $m$ 而非 $n$ 小於 $m$。如果使用這式子，那麼要將上面給出的除法定義，
轉化為邱奇編碼的自然數函數如下，

$\mathrm{divide1}nmfx=(\lambda d.\mathrm{IsZero}d(0fx)(f(\mathrm{divide1}dmfx)))(\mathrm{minus}nm)$

這樣的定義只呼叫了一次 $n$ 減去 $m$，正如我們所想的。然而問題是這式子計算成錯誤的結果，
是 (n-1)/m 除法的商。要更正則需在呼叫 divide 之前把 $n$ 再加回 1。 因此除法的正確定義是，

$\mathrm{divide}n=\mathrm{divide1}(\mathrm{succ}n)$

divide1 是一個內含遞迴的定義式，要以 Y 組合子來發生遞迴作用。 所以要再宣告一個名為 div 的新函數；

• 等號左側為 divide1 → div c
• 等號右側為 divide1 → c

要獲得

$\mathrm{div}=\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.\mathrm{IsZero}d(0fx)(f(cdmfx)))(\mathrm{minus}nm)$

那麼

$\mathrm{divide}=\lambda n.\mathrm{divide1}(\mathrm{succ}n)$

而式中所用的其它函式定義如下列：

$\begin{array}{cc}\mathrm{divide1}& =Y\mathrm{div}\\ \mathrm{succ}& =\lambda n.\lambda f.\lambda x.f(nfx)\\ Y& =\lambda f.(\lambda x.f(xx))(\lambda x.f(xx))\\ 0& =\lambda f.\lambda x.x\\ \mathrm{IsZero}& =\lambda n.n(\lambda x.\mathrm{false})\mathrm{true}\end{array}$

$\begin{array}{cc}\mathrm{true}& \equiv \lambda a.\lambda b.a\\ \mathrm{false}& \equiv \lambda a.\lambda b.b\end{array}$

$\begin{array}{cc}\mathrm{minus}& =\lambda m.\lambda n.n\mathrm{pred}m\\ \mathrm{pred}& =\lambda n.\lambda f.\lambda x.n(\lambda g.\lambda h.h(gf))(\lambda u.x)(\lambda u.u)\end{array}$

使用倒斜線 \ 代替 λ 符號，完整的除法函式則如下列，

divide = (\n.((\f.(\x.x x) (\x.f (x x))) (\c.\n.\m.\f.\x.(\d.(\n.n (\x.(\a.\b.b)) (\a.\b.a)) d ((\f.\x.x) f x) (f (c d m f x))) ((\m.\n.n (\n.\f.\x.n (\g.\h.h (g f)) (\u.x) (\u.u)) m) n m))) ((\n.\f.\x. f (n f x)) n))

換成其它表達法

大部分真實世界的程式語言都提供原生於機器的整數，church 與 unchurch 函式會在整數及與之對應的邱奇數間轉換。這裡使用Haskell撰寫函式， \ 等同於lambda演算的 λ。 用其它語言表達也會很類似。

type Church a = (a -> a) -> a -> a

church :: Integer -> Church Integer
church 0 = \f -> \x -> x
church n = \f -> \x -> f (church (n-1) f x)

unchurch :: Church Integer -> Integer
unchurch cn = cn (+ 1) 0

邱奇布尔值

邱奇布尔值是布尔值真和假的邱奇编码形式。某些程式語言使用這個方式來實踐布爾算術的模型，Smalltalk 即為一例。

布爾邏輯可以想成二選一，而布尔值則表示为有两个参数的函数，它得到两个参数中的一个：

• 真 則選擇第一個參數
• 假 則選擇第二個參數

邱奇布爾值在lambda演算中的形式定义如下：

$\begin{array}{cc}\mathrm{true}& \equiv \lambda a.\lambda b.a\\ \mathrm{false}& \equiv \lambda a.\lambda b.b\end{array}$

由於真、假 可以選擇第一個或第二個參數，所以其能夠由組合來產生邏輯運算子。注意到 not 版本因不同求值策略而有兩個。下列為从邱奇布尔值推导来的布尔算术的函数：

$\begin{array}{cc}\mathrm{and}& =\lambda p.\lambda q.pqp\\ \mathrm{or}& =\lambda p.\lambda q.ppq\\ {\mathrm{not}}_1& =\lambda p.\lambda a.\lambda b.pba{}^{\text{*1}}\\ {\mathrm{not}}_2& =\lambda p.p(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=\lambda p.p\mathrm{false}\mathrm{true}{}^{\text{*2}}\\ \mathrm{xor}& =\lambda a.\lambda b.a(\mathrm{not}b)b\\ \mathrm{if}& =\lambda p.\lambda a.\lambda b.pab\end{array}$

註：

• ¹ 求值策略使用應用次序時，這個方法才正確。
• ² 求值策略使用正常次序時，這個方法才正確。

下頭為一些範例：

$\begin{array}{cc}\mathrm{and}\mathrm{true}\mathrm{false}& =(\lambda p.\lambda q.pqp)\mathrm{true}\mathrm{false}=\mathrm{true}\mathrm{false}\mathrm{true}=(\lambda a.\lambda b.a)\mathrm{false}\mathrm{true}=\mathrm{false}\\ \mathrm{or}\mathrm{true}\mathrm{false}& =(\lambda p.\lambda q.ppq)(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)=\mathrm{true}\\ {\mathrm{not}}_1\mathrm{true}& =(\lambda p.\lambda a.\lambda b.pba)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)ba=\lambda a.\lambda b.(\lambda c.b)a=\lambda a.\lambda b.b=\mathrm{false}\\ {\mathrm{not}}_2\mathrm{true}& =(\lambda p.p(\lambda a.\lambda b.b)(\lambda a.\lambda b.a))(\lambda a.\lambda b.a)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=(\lambda b.(\lambda a.\lambda b.b))(\lambda a.\lambda b.a)=\lambda a.\lambda b.b=\mathrm{false}\end{array}$

参见

• Lambda演算
• 系统F，在有类型lambda演算中的邱奇数

外部链接

• Some interactive examples of Church numerals Template:Wayback