Church数

**邱奇編碼**是把數據和運算符嵌入到 lambda 演算內的一種方式，最常見的形式即邱奇數，它使用 lambda 符號表示自然數。方法得名於阿隆佐・邱奇，他首先以這種方法把數據編碼到 lambda 演算中。

透過邱奇編碼，在其他符號系統中通常被認定為基本的項（比如整數、布爾值、有序對、列表和 tagged unions）都會被映射到高階函數。在無型別 lambda 演算，函數是唯一的原始型別。

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

很多學數學的學生熟悉可計算函數集合的哥德爾編號；邱奇編碼是定義在 lambda 抽象而不是自然數上的等價運算。

## 邱奇數

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

　
: $f^{\circ n}=\underbrace {f\circ f\circ \cdots \circ f} _{n{\text{ 次}}}.\,$

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

　
: ${\begin{array}{r|l|l}{\text{ 自 然 數}}&{\text{函 數 定 義}}&{\text{lambda 表 達 式}}\\\hline 0&0\ f\ x=x&0=\lambda f.\lambda x.x\\1&1\ f\ x=f\ x&1=\lambda f.\lambda x.f\ x\\2&2\ f\ x=f\ (f\ x)&2=\lambda f.\lambda x.f\ (f\ x)\\3&3\ f\ x=f\ (f\ (f\ x))&3=\lambda f.\lambda x.f\ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\ f\ x=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{cases}0&{\mbox{if }}n=0,\\n-1&{\mbox{otherwise}}\end{cases}}$ 通過生成每次都應用它們的參數 `g` 於 `f` 的 $n$ 重函數複合來工作；基礎情況丟棄它的 `f` 複本並返回 `x`。

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

### 邱奇數函數一表

\* 注意在邱奇編碼中，

 * $\operatorname {pred} (0)=0$
* $m<n\to m-n=0$

 

### 除法函式

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

　
: $n/m=\operatorname {if} \ n\geq m\ \operatorname {then} \ 1+(n-m)/m\ \operatorname {else} \ 0$

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

　
: $\operatorname {IsZero} \ (\operatorname {minus} \ n\ m)$

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

　
: $\operatorname {divide1} \ n\ m\ f\ x=(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (\operatorname {divide1} \ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)$

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

　
: $\operatorname {divide} \ n=\operatorname {divide1} \ (\operatorname {succ} \ n)$

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

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

 
要獲得

　
: $\operatorname {div} =\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)$

 
那麼

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

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

　
: ${\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\0&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}$

　
: ${\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}$

　
: ${\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}$

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

```
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 演算的 λ。 用其它語言表達也會很類似。

## 邱奇布爾值

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

布爾邏輯可以想成二選一，而布爾值則表示為有兩個參數的函數，它得到兩個參數中的一個：

* _真_ 則選擇第一個參數
* _假_ 則選擇第二個參數

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

　
: ${\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}$

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

　
: ${\begin{aligned}\operatorname {and} &=\lambda p.\lambda q.p\ q\ p\\\operatorname {or} &=\lambda p.\lambda q.p\ p\ q\\\operatorname {not} _{1}&=\lambda p.\lambda a.\lambda b.p\ b\ a\ ^{\scriptstyle {\text{*1}}}\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \ ^{\scriptstyle {\text{*2}}}\\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}$

_註：_

* _1 求值策略使用應用次序時，這個方法才正確。_
* _2 求值策略使用正常次序時，這個方法才正確。_

 
下頭為一些範例：

　
: ${\begin{aligned}\operatorname {and} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} =\operatorname {true} \operatorname {false} \operatorname {true} =(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} =\operatorname {false} \\\operatorname {or} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ p\ q)\ (\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)=\operatorname {true} \\\operatorname {not} _{1}\ \operatorname {true} &=(\lambda p.\lambda a.\lambda b.p\ b\ a)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a=\lambda a.\lambda b.(\lambda c.b)\ a=\lambda a.\lambda b.b=\operatorname {false} \\\operatorname {not} _{2}\ \operatorname {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=\operatorname {false} \end{aligned}}$

## 參見

* Lambda 演算
* 系統 F，在有類型 lambda 演算中的邱奇數

## 外部連結

* Some interactive examples of Church numerals （頁面存檔備份，存於網際網路檔案館）