邱奇數

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

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

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

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

用途

直接實現邱奇編碼會將某些訪問操作的時間複雜度從 $O(1)$ 降低到 $O(n)$ （其中 $n$ 是資料結構的大小），這使得該編碼方式在實際應用中受到限制。^[1]研究表明可以通過針對性優化解決這個問題，但大多數函數式編程語言選擇擴展其中間表示以包含代數數據類型。^[2] 儘管如此，邱奇編碼仍常用於理論論證，因為它在部分求值和定理證明中具有自然表示優勢。^[1]通過使用高階類型可以對操作進行類型標註，^[3]並能便捷地實現原始遞歸。^[1]由於函數被假定為唯一的原始數據類型，這種設定簡化了許多證明過程。

邱奇編碼具有表示完整性但僅限於表徵層面。需要額外函數將這種表示轉換為通用數據類型以供人工解讀。由於邱奇定理中等價性不可判定，通常無法判斷兩個函數是否具有外延等價性。轉換過程可能需要通過某種方式應用函數來提取其表徵值，或者以λ項字面量的形式查找其值。λ演算通常被解釋為使用內涵等價性。由於等價性的內涵定義與外延定義存在差異，在結果解釋方面可能存在潛在問題。

邱奇數

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

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

不論邱奇數為何，其都是接受兩個參數的函數。邱奇數0、1、2、... 在λ演算中的定義如下：

從 0 不應用函數開始， 1 應用函數一次， 2 應用函數兩次， 3 應用函數三次，依此類推：

{\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}}

邱奇數3表示對任意給定函數應用三次的操作。當輸入函數被提供時，首先應用於初始參數，然後連續應用於自身結果。最終結果並非數字3（除非初始參數恰好為0且函數為後繼函數）。邱奇數3的本質是函數的應用次數，而非計算結果本身。其核心意義在於「重複三次」的動作，這正是「三次」概念的直觀體現。

就是說，自然數 $n$ 被表示為邱奇數n，它對於任何lambda-項F和X有著性質：

n F X =_β Fⁿ X。

使用邱奇數的計算

在 lambda 演算中，數值函數被表示為在邱奇數上的相應函數。這些函數在大多數函數式語言中可以通過 lambda 項的直接變換來實現（服從於類型約束）（請參閱將lambda表達式轉換為函數）。

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

\operatorname {plus} \equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)

後繼函數 ${\text{succ}}(n)=n+1$ β-等價於（plus 1）。

\operatorname {succ} \equiv \lambda n.\lambda f.\lambda x.f\ (n\ f\ x)

乘法函數 ${\text{mult}}(m,n)=m\times n$ 利用了恆等式 $f^{\circ (m\times n)}=(f^{\circ n})^{\circ m}(x)$ 。

\operatorname {mult} \equiv \lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x

指數函數 $\exp(b,n)=b^{n}$ 通過邱奇數定義給出：將定義中的 $h\to b$ 和 $x\to f$ 代入 $n\ h\ x=h^{n}\ x$ 可得 $n\ b\ f=b^{n}\ f$ ，因此：

\operatorname {exp} \ b\ n=b^{n}=n\ b

對應的lambda表達式為：

\operatorname {exp} \equiv \lambda b.\lambda n.n\ b

前驅函數 ${\text{pred}}(n)$ 的實現較為複雜：

\operatorname {pred} \equiv \lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)

邱奇數通過n次應用函數來運作。前驅函數需要返回一個應用參數n-1次的函數。這通過構建包含f和x的容器來實現，該容器以省略第一次函數應用的方式初始化（詳見前驅函數推導）。

基於前驅函數可定義減法函數：

\operatorname {minus} \equiv \lambda m.\lambda n.(n\operatorname {pred} )\ m

邱奇數函數一表

函數	代數	等同	函數定義	Lambda 表達式
後繼	$n+1$	$f^{n+1}\ x=f(f^{n}x)$	$\operatorname {succ} \ n\ f\ x=f\ (n\ f\ x)$	$\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)$	...
加法	$m+n$	$f^{m+n}\ x=f^{m}(f^{n}x)$	$\operatorname {plus} \ m\ n\ f\ x=m\ f\ (n\ f\ x)$	$\lambda m.\lambda n.\lambda f.\lambda x.m\ f\ (n\ f\ x)$	$\lambda m.\lambda n.n\operatorname {succ} m$
乘法	$m\times n$	$f^{m\times n}\ x=(f^{m})^{n}\ x$	$\operatorname {multiply} \ m\ n\ f\ x=m\ (n\ f)\ x$	$\lambda m.\lambda n.\lambda f.\lambda x.m\ (n\ f)\ x$	$\lambda m.\lambda n.\lambda f.m\ (n\ f)$
指數	$b^{n}$	$n\ b\ f=b^{n}\ f$ ^[a]	$\operatorname {exp} \ b\ n\ f\ x=n\ b\ f\ x$	$\lambda b.\lambda n.\lambda f.\lambda x.n\ b\ f\ x$	$\lambda b.\lambda n.n\ b$
前驅^[b]	$n-1$	$\operatorname {inc} ^{n}\operatorname {con} =\operatorname {val} (f^{n-1}x)$	$if(n==0)\ 0\ else\ (n-1)$	$\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)$
減法^[b]	$m-n$	$f^{m-n}\ x=(f^{-1})^{n}(f^{m}x)$	$\operatorname {minus} \ m\ n=(n\operatorname {pred} )\ m$	...	$\lambda m.\lambda n.n\operatorname {pred} m$

注意：

^ 此公式是邱奇數 $n$ 的定義，其中 $f\to b,x\to f$ 。
^ ^2.0 ^2.1
在邱奇編碼中，
- $\operatorname {pred} (0)=0$
- $m\leq n\to m-n=0$

前驅函數推導

邱奇編碼中使用的前驅函數定義為：

\operatorname {pred} (n)={\begin{cases}0&{\mbox{ 若 }}n=0,\\n-1&{\mbox{ 否 则 }}\end{cases}}

為了減少一次函數應用次數來構造前驅函數，需採用容器函數封裝值。定義新函數 $inc$ 和 $init$ 替代原函數 $f$ 和參數 $x$ ，其中容器函數稱為 $value$ 。下表左側展示了邱奇數 $n$ 作用於 $inc$ 和 $init$ 的情況：

{\begin{array}{r|r|r}{\text{ 邱 奇 数 }}&{\text{ 使 用 init}}&{\text{ 使 用 const}}\\\hline 0&\operatorname {init} =\operatorname {value} \ x&\\1&\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f\ x)&\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x\\2&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} )=\operatorname {value} \ (f\ (f\ x))&\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} )=\operatorname {value} \ (f\ x)\\3&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {init} ))=\operatorname {value} \ (f\ (f\ (f\ x)))&\operatorname {inc} \ (\operatorname {inc} \ (\operatorname {inc} \ \operatorname {const} ))=\operatorname {value} \ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\operatorname {inc} \ \operatorname {init} =\operatorname {value} \ (f^{n}\ x)=\operatorname {value} \ (n\ f\ x)&n\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ (f^{n-1}\ x)=\operatorname {value} \ ((n-1)\ f\ x)\\\end{array}}

通用遞歸規則為：

\operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)

若定義從容器中提取值的函數 $extract$ ：

\operatorname {extract} \ (\operatorname {value} \ v)=v

則可構造同數函數 $samenum$ ：

\operatorname {samenum} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {init} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ (n\ f\ x))=\lambda n.\lambda f.\lambda x.n\ f\ x=\lambda n.n

通過將 $init$ 替換為特殊容器 $const$ （該容器首次調用時忽略參數以跳過第一次函數應用），可推導前驅函數：

\operatorname {pred} =\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (n\operatorname {inc} \operatorname {const} )=\lambda n.\lambda f.\lambda x.\operatorname {extract} \ (\operatorname {value} \ ((n-1)\ f\ x))=\lambda n.\lambda f.\lambda x.(n-1)\ f\ x=\lambda n.(n-1)

具體函數定義如下：

{\begin{aligned}\operatorname {value} &=\lambda v.(\lambda h.h\ v)\\\operatorname {extract} k&=k\ \lambda u.u\\\operatorname {inc} &=\lambda g.\lambda h.h\ (g\ f)\\\operatorname {init} &=\lambda h.h\ x\\\operatorname {const} &=\lambda u.x\end{aligned}}

最終得到前驅函數的lambda表達式：

\operatorname {pred} =\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)

值容器 [編輯] 值容器將函數作用於其內部值，定義為： $\operatorname {value} \ v\ h=h\ v$ 即： $\operatorname {value} =\lambda v.(\lambda h.h\ v)$ Inc函數 [編輯] $inc$ 函數需接收包含 $v$ 的容器，返回包含 $f v$ 的新容器： $\operatorname {inc} \ (\operatorname {value} \ v)=\operatorname {value} \ (f\ v)$ 設 $g$ 為值容器： $g=\operatorname {value} \ v$ 則： $g\ f=\operatorname {value} \ v\ f=f\ v$ 因此： $\operatorname {inc} \ g=\operatorname {value} \ (g\ f)$ $\operatorname {inc} =\lambda g.\lambda h.h\ (g\ f)$	提取函數 [編輯] 通過應用恆等函數提取值： $I=\lambda u.u$ 利用 $I$ 可得： $\operatorname {value} \ v\ I=v$ 故： $\operatorname {extract} \ k=k\ I$ Const容器 [編輯] 為實現 $pred$ 函數，需將 $init$ 替換為不應用 $f$ 的 $const$ 容器。該容器需滿足： $\operatorname {inc} \ \operatorname {const} =\operatorname {value} \ x$ $\lambda h.h\ (\operatorname {const} \ f)=\lambda h.h\ x$ 當滿足條件： $\operatorname {const} \ f=x$ 對應的lambda表達式為： $\operatorname {const} =\lambda u.x$

前驅函數的另一種解釋

使用組合子符號可簡化前驅函數的解釋：

Kxy=x

Ix=x

Xfri=i(rf)

Pred\ nfx=n(Xf)(Kx)I

通過下列推導可驗證其正確性：

Pred\ (Succ\ n)fx=Succ\ n(Xf)(Kx)I=Xf(n(Xf)(Kx))I

\ \ \ \ =I(n(Xf)(Kx)f)=\ ...\ =I(f(f...(f(Kxf))...))=I(nfx)=nfx

Pred\ Zero\ fx=\ Zero(Xf)(Kx)I=\ KxI=\ x=\ Zero\ fx

通過eta-歸約和歸納法可得：

Pred\ (Succ\ n)=n

Pred\ Zero=Zero

Pred\ (Pred\ Zero)=\ Pred\ Zero=\ Zero

前驅函數的另一種定義

使用序對可定義前驅函數：

{\begin{aligned}\operatorname {f} =&\ \lambda p.\ \operatorname {pair} \ (\operatorname {second} \ p)\ (\operatorname {succ} \ (\operatorname {second} \ p))\\\operatorname {zero} =&\ (\lambda f.\lambda x.\ x)\\\operatorname {pc0} =&\ \operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} \\\operatorname {pred} =&\ \lambda n.\ \operatorname {first} \ (n\ \operatorname {f} \ \operatorname {pc0} )\\\end{aligned}}

此定義雖簡潔但展開式較複雜，以 $\operatorname {pred} \operatorname {three}$ 為例：

{\begin{aligned}\operatorname {pred} \operatorname {three} =&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {zero} ))))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {zero} \ \operatorname {one} )))\\=&\ \operatorname {first} \ (\operatorname {f} \ (\operatorname {pair} \ \operatorname {one} \ \operatorname {two} ))\\=&\ \operatorname {first} \ (\operatorname {pair} \ \operatorname {two} \ \operatorname {three} )\\=&\ \operatorname {two} \end{aligned}}

除法函式

自然數除法可通過以下方式實現：^[4]

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\leq 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)

此定義僅調用一次 $\operatorname {minus} \ n\ m$ ，但結果為此公式給出的是 $(n-1)/m$ 的值。

通過給n加1後調用divide可修正該問題，定義式為：

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

divide1為遞歸定義，需用Y組合子實現遞歸。通過以下步驟創建新函數div：

左側替換： $\operatorname {divide1} \rightarrow \operatorname {div} \ c$
右側替換： $\operatorname {divide1} \rightarrow 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}}

最終展開式：

\scriptstyle \operatorname {divide} =\lambda n.((\lambda f.(\lambda x.x\ x)\ (\lambda x.f\ (x\ x)))\ (\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.(\lambda n.n\ (\lambda x.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a))\ d\ ((\lambda f.\lambda x.x)\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ ((\lambda m.\lambda n.n(\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u))m)\ n\ m)))\ ((\lambda n.\lambda f.\lambda x.f\ (n\ f\ x))\ n)

以文本格式表示（用\代替λ）：

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))

例如，9/3可表示為：

divide (\f.\x.f (f (f (f (f (f (f (f (f x))))))))) (\f.\x.f (f (f x)))

使用lambda演算計算器，按正規順序歸約後結果為3：

\f.\x.f (f (f (x)))

有符號數

通過使用包含正負值的邱奇序對，可將邱奇數擴展至有符號數^[5]。整數值即兩個邱奇數的差值。

自然數轉有符號數的定義為：

\operatorname {convert} _{s}=\lambda x.\operatorname {pair} \ x\ 0

取反操作通過交換序對元素實現：

\operatorname {neg} _{s}=\lambda x.\operatorname {pair} \ (\operatorname {second} \ x)\ (\operatorname {first} \ x)

當序對中某一元素為零時，整數表示更自然。OneZero函數確保該條件：

\operatorname {OneZero} =\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))

使用Y組合子實現遞歸：

\operatorname {OneZ} =\lambda c.\lambda x.\operatorname {IsZero} \ (\operatorname {first} \ x)\ x\ (\operatorname {IsZero} \ (\operatorname {second} \ x)\ x\ (c\ (\operatorname {pair} \ (\operatorname {pred} \ (\operatorname {first} \ x))\ (\operatorname {pred} \ (\operatorname {second} \ x)))))

\operatorname {OneZero} =Y\operatorname {OneZ}

加減運算

加法數學定義為：

x+y=[x_{p},x_{n}]+[y_{p},y_{n}]=(x_{p}+y_{p})-(x_{n}+y_{n})=[x_{p}+y_{p},x_{n}+y_{n}]

對應lambda表達式：

\operatorname {plus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))

減法定義為：

x-y=[x_{p},x_{n}]-[y_{p},y_{n}]=(x_{p}+y_{n})-(x_{n}+y_{p})=[x_{p}+y_{n},x_{n}+y_{p}]

對應lambda表達式：

\operatorname {minus} _{s}=\lambda x.\lambda y.\operatorname {OneZero} \ (\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {plus} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))

乘除運算

乘法定義為：

x*y=(x_{p}*y_{p}+x_{n}*y_{n})-(x_{p}*y_{n}+x_{n}*y_{p})=[x_{p}*y_{p}+x_{n}*y_{n},x_{p}*y_{n}+x_{n}*y_{p}]

對應lambda表達式：

\operatorname {mult} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {mult} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {mult} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))

除法需確保序對元素含零（見上文的OneZero），定義輔助函數：

\operatorname {divZ} =\lambda x.\lambda y.\operatorname {IsZero} \ y\ 0\ (\operatorname {divide} \ x\ y)

除法表達式：

\operatorname {divide} _{s}=\lambda x.\lambda y.\operatorname {pair} \ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {first} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {second} \ y)))\ (\operatorname {plus} \ (\operatorname {divZ} \ (\operatorname {first} \ x)\ (\operatorname {second} \ y))\ (\operatorname {divZ} \ (\operatorname {second} \ x)\ (\operatorname {first} \ y)))

有理數與實數

有理數可表示為有符號數序對，可計算實數可通過極限過程編碼^[6]^[7]。複數可自然地表示為實數序對。上述數據類型驗證了邱奇-圖靈論題：任何數據類型或計算均可編碼於lambda演算中。

換成其它表達法

大部分真實世界的程式語言都提供原生於機器的整數，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和Pico即為典型示例。

布爾邏輯本質上是選擇機制。邱奇布爾值的編碼形式為接收兩個參數的函數：

真（true）選擇第一個參數
假（false）選擇第二個參數

其標準定義為：

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

這種編碼允許謂詞函數（返回邏輯值的函數）直接作為條件語句使用。當布爾函數作用於兩個參數時，將根據真值返回其中一個參數：

\operatorname {predicate-} x\ \operatorname {then-clause} \ \operatorname {else-clause}

若predicate-x為真則返回then-clause，否則返回else-clause。

由於真值與假值的選擇特性，它們可組合出各類邏輯運算符。需注意邏輯非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\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}

註：

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

運算示例解析：

{\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}}

謂詞

謂詞是返回布爾值的函數。最基礎的謂詞是 $\operatorname {IsZero}$ ，當其參數為邱奇數 $0$ 時返回 $\operatorname {true}$ ，否則返回 $\operatorname {false}$ ：

\operatorname {IsZero} =\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true}

下列謂詞檢測第一個參數是否小於等於第二個參數：

\operatorname {LEQ} =\lambda m.\lambda n.\operatorname {IsZero} \ (\operatorname {minus} \ m\ n)

基於恆等關係：

x=y\equiv (x\leq y\land y\leq x)

相等性檢測可定義為：

\operatorname {EQ} =\lambda m.\lambda n.\operatorname {and} \ (\operatorname {LEQ} \ m\ n)\ (\operatorname {LEQ} \ n\ m)

邱奇序對

邱奇序對是二元組的邱奇編碼實現。序對被表示為接收函數的函數，當傳入參數時會將該參數作用於序對的兩個分量。其lambda演算定義為：

{\begin{aligned}\operatorname {pair} &\equiv \lambda x.\lambda y.\lambda z.z\ x\ y\\\operatorname {first} &\equiv \lambda p.p\ (\lambda x.\lambda y.x)\\\operatorname {second} &\equiv \lambda p.p\ (\lambda x.\lambda y.y)\end{aligned}}

示例推導：

{\begin{aligned}&\operatorname {first} \ (\operatorname {pair} \ a\ b)\\=&(\lambda p.p\ (\lambda x.\lambda y.x))\ ((\lambda x.\lambda y.\lambda z.z\ x\ y)\ a\ b)\\=&(\lambda p.p\ (\lambda x.\lambda y.x))\ (\lambda z.z\ a\ b)\\=&(\lambda z.z\ a\ b)\ (\lambda x.\lambda y.x)\\=&(\lambda x.\lambda y.x)\ a\ b=a\end{aligned}}

列表編碼

不可變的列表由列表節點構成，其基本操作包括：

函數	描述
nil	構造空列表
isnil	檢測列表是否為空
cons	在列表頭部添加元素
head	獲取列表首元素
tail	獲取列表尾部

以下給出四種不同的列表表示法：

使用雙序對構造列表節點（支持空列表）
使用單序對構造列表節點
基於右摺疊函數的列表表示
採用Scott編碼的模式匹配參數化表示

雙序對列表節點

非空列表可用邱奇序對表示：

First 存儲首元素
Second 存儲尾部

為支持空列表，需額外包裹序對形成三層結構：

First - 空列表標識符
Second.First 存儲首元素
Second.Second 存儲尾部

基於此的核心操作定義如下：^[8]

表達式	描述
$\operatorname {nil} \equiv \operatorname {pair} \ \operatorname {true} \ \operatorname {true}$	序對首元素為true表示空列表
$\operatorname {isnil} \equiv \operatorname {first}$	提取空列表標識符
$\operatorname {cons} \equiv \lambda h.\lambda t.\operatorname {pair} \operatorname {false} \ (\operatorname {pair} h\ t)$	構造非空列表節點
$\operatorname {head} \equiv \lambda z.\operatorname {first} \ (\operatorname {second} z)$	通過second.first獲取首元素
$\operatorname {tail} \equiv \lambda z.\operatorname {second} \ (\operatorname {second} z)$	通過second.second獲取尾部

注意：當列表為空時，head和tail函數不應被調用。

單序對列表節點

另一種定義方式^[9]：

{\begin{aligned}\operatorname {cons} &\equiv \operatorname {pair} \\\operatorname {head} &\equiv \operatorname {first} \\\operatorname {tail} &\equiv \operatorname {second} \\\operatorname {nil} &\equiv \operatorname {false} \\\operatorname {isnil} &\equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\operatorname {false} )\operatorname {true} \\\end{aligned}}

通用處理模板定義為：

{\begin{aligned}\operatorname {process-list} &\equiv \lambda l.l(\lambda h.\lambda t.\lambda d.\operatorname {head-and-tail-clause} )\operatorname {nil-clause} \\\end{aligned}}

其他擴展操作：

{\begin{aligned}\operatorname {tail-or-nil} &\equiv \lambda l.\ l\ (\lambda h.\lambda t.\lambda d.\ t)\ \operatorname {nil} \\\operatorname {fold} &\equiv \lambda f.\ \operatorname {Y} \ (\lambda r.\lambda a.\lambda l.\ l\ (\lambda h.\lambda t.\lambda d.\ r\ (f\ a\ h)\ t)\ a)\\\operatorname {rfold} &\equiv \lambda f.\lambda a.\ \operatorname {Y} \ (\lambda r.\lambda l.\ l\ (\lambda h.\lambda t.\lambda d.\ f\ (r\ t)\ h)\ a)\\\operatorname {length} &\equiv \operatorname {fold} \ (\lambda a.\lambda h.\ \operatorname {succ} \ a)\ \operatorname {zero} \end{aligned}}

{\begin{aligned}\operatorname {map} &\equiv \lambda f.\lambda l.\ \operatorname {rfold} \ (\lambda a.\lambda h.\ \operatorname {cons} \ (f\ h)\ a)\ \operatorname {nil} \ l\\&\equiv \lambda f.\ \operatorname {rfold} \ (\lambda a.\lambda h.\ \operatorname {cons} \ (f\ h)\ a)\ \operatorname {nil} \\\operatorname {filter} &\equiv \lambda f.\lambda l.\ \operatorname {rfold} \ (\lambda a.\lambda h.\ f\ h\ (\operatorname {cons} \ h\ a)\ a)\ \operatorname {nil} \ l\\&\equiv \lambda f.\ \operatorname {rfold} \ (\lambda a.\lambda h.\ f\ h\ (\operatorname {cons} \ h\ a)\ a)\ \operatorname {nil} \\\operatorname {reverse} &\equiv \lambda l.\ \operatorname {fold} \ (\lambda a.\lambda h.\ \operatorname {cons} \ h\ a)\ \operatorname {nil} \ l\\&\equiv \operatorname {fold} \ (\lambda a.\lambda h.\ \operatorname {cons} \ h\ a)\ \operatorname {nil} \\\operatorname {concat} &\equiv \lambda l.\lambda g.\ \operatorname {rfold} \ (\lambda a.\lambda h.\ \operatorname {cons} \ h\ a)\ g\ l\\\operatorname {append} &\equiv \lambda l.\lambda v.\ \operatorname {concat} \ l\ (\operatorname {cons} \ v\ \operatorname {nil} )\end{aligned}}

{\begin{aligned}\operatorname {skip} &\equiv \lambda n.\lambda l.\ n\ \operatorname {tail-or-nil} \ l\\&\equiv \lambda n.\ n\ \operatorname {tail-or-nil} \\&\equiv \operatorname {Y} \ (\lambda r.\lambda n.\lambda l.\ l\ (\lambda h.\lambda t.\lambda d.\ \operatorname {IsZero} \ n\ l\ (r\ (\operatorname {pred} \ n)\ t))\ \operatorname {nil} )\\\operatorname {skip-last} &\equiv \lambda n.\lambda l.\ \operatorname {IsZero} \ n\ l\ \operatorname {second} (\\&\ \ \ \ \operatorname {Y} \ (\lambda r.\lambda lr.\ lr\ (\lambda h.\lambda t.\lambda d.\\&\ \ \ \ \ \ \ \ r\ t\ (\lambda na.\lambda la.\ \operatorname {IsZero} \ na\\&\ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ \operatorname {zero} \ (\operatorname {cons} \ h\ la))\\&\ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ (\operatorname {pred} \ na)\ \operatorname {nil} )\\&\ \ \ \ \ \ \ \ ))\\&\ \ \ \ \ \ \ \ (\operatorname {pair} \ n\ \operatorname {nil} )\\&\ \ \ \ )\ l)\\\operatorname {skip-while} &\equiv \lambda f.\ \operatorname {Y} \ (\lambda r.\lambda l.\ l\ (\lambda h.\lambda t.\lambda d.\ f\ h\ (r\ t)\ l)\ \operatorname {nil} )\\\operatorname {take} &\equiv \operatorname {Y} \ (\lambda r.\lambda n.\lambda l.\ l\ (\lambda h.\lambda t.\lambda d.\ \operatorname {IsZero} \ n\ \operatorname {nil} \ (\operatorname {cons} \ h\ (r\ (\operatorname {pred} \ n)\ t)))\ \operatorname {nil} )\\\operatorname {take-last} &\equiv \lambda n.\lambda l.\ \operatorname {IsZero} \ n\ l\ \operatorname {second} (\\&\ \ \ \ \operatorname {Y} \ (\lambda r.\lambda lr.\ lr\ (\lambda h.\lambda t.\lambda d.\\&\ \ \ \ \ \ \ \ r\ t\ (\lambda na.\lambda la.\ \operatorname {IsZero} \ na\\&\ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ \operatorname {zero} \ la)\\&\ \ \ \ \ \ \ \ \ \ \ \ (\operatorname {pair} \ (\operatorname {pred} \ na)\ lr)\\&\ \ \ \ \ \ \ \ ))\\&\ \ \ \ \ \ \ \ (\operatorname {pair} \ n\ \operatorname {nil} )\\&\ \ \ \ )\ l)\\\operatorname {take-while} &\equiv \lambda f.\ \operatorname {Y} \ (\lambda r.\lambda l.\ l\ (\lambda h.\lambda t.\lambda d.\ f\ d\ (\operatorname {cons} \ h\ (r\ t))\ \operatorname {nil} )\ \operatorname {nil} )\end{aligned}}

{\begin{aligned}\operatorname {all} &\equiv \operatorname {Y} \ (\lambda r.\lambda f.\lambda l.\ l\ (\lambda h.\lambda t.\lambda d.\ f\ h\ (r\ f\ t)\ \operatorname {false} )\ \operatorname {true} )\\\operatorname {any} &\equiv \operatorname {Y} \ (\lambda r.\lambda f.\lambda l.\ l\ (\lambda h.\lambda t.\lambda d.\ f\ h\ \operatorname {true} \ (r\ f\ t))\ \operatorname {false} )\\\operatorname {element-at} &\equiv \lambda n.\lambda l.\ \operatorname {head} \ (\operatorname {skip} \ n\ l)\\\operatorname {insert-at} &\equiv \lambda n.\lambda v.\lambda l.\ \operatorname {concat} \ (\operatorname {take} \ n\ l)\ (\operatorname {cons} \ v\ (\operatorname {skip} \ n\ l))\\\operatorname {remove-at} &\equiv \lambda n.\lambda l.\ \operatorname {concat} \ (\operatorname {take} \ n\ l)\ (\operatorname {skip} \ (\operatorname {succ} \ n)\ l)\\\operatorname {replace-at} &\equiv \lambda n.\lambda v.\lambda l.\ \operatorname {concat} \ (\operatorname {take} \ n\ l)\ (\operatorname {cons} \ v\ (\operatorname {skip} \ (\operatorname {succ} \ n)\ l))\\\operatorname {index-of} &\equiv \lambda f.\ \operatorname {Y} \ (\lambda r.\lambda n.\lambda l.\ l\ (\lambda h.\lambda t.\lambda d.\ f\ h\ n\ (r\ (\operatorname {succ} \ n)\ t))\ \operatorname {zero} )\ \operatorname {one} \\\operatorname {last-index-of} &\equiv \lambda f.\ \operatorname {Y} \ (\lambda r.\lambda n.\lambda l.\ l\ (\lambda h.\lambda t.\lambda d.\ (\lambda i.\ \operatorname {IsZero} \ i\ (f\ h\ n\ \operatorname {zero} )\ i)\ (r\ (\operatorname {succ} \ n)\ t))\ \operatorname {zero} )\ \operatorname {one} \\\operatorname {range} &\equiv \lambda f.\lambda z.\ \operatorname {Y} \ (\lambda r.\lambda s.\lambda n.\ \operatorname {IsZero} \ n\ \operatorname {nil} \ (\operatorname {cons} \ (s\ f\ z)\ (r\ (\operatorname {succ} \ s)\ (\operatorname {pred} \ n))))\ \operatorname {zero} \\\operatorname {repeat} &\equiv \lambda v.\ \operatorname {Y} \ (\lambda r.\lambda n.\ \operatorname {IsZero} \ n\ \operatorname {nil} \ (\operatorname {cons} \ v\ (r\ (\operatorname {pred} \ n))))\\\operatorname {zip} &\equiv Y\ (\lambda r.\lambda l1.\lambda l2.\ l1\ (\lambda h1.\lambda t1.\lambda d1.\ l2\ (\lambda h2.\lambda t2.\lambda d2.\ \operatorname {cons} \ (\operatorname {pair} \ h1\ h2)\ (r\ t1\ t2))\ \operatorname {nil} )\ \operatorname {nil} )\\\end{aligned}}

右摺疊列表表示

作為邱奇序對編碼的替代方案，列表可通過其右摺疊函數進行編碼。例如，包含三個元素x、y、z的列表可編碼為高階函數，當該函數應用組合子c和初始值n時，返回c x (c y (c z n))。這等價於部分應用函數組合鏈的調用：(c x ∘ c y ∘ c z) n。

{\begin{aligned}\operatorname {nil} &\equiv \lambda c.\lambda n.n\\\operatorname {singleton} &\equiv \lambda h.\lambda c.\lambda n.c\ h\ n\\\operatorname {cons} &\equiv \lambda h.\lambda t.\lambda c.\lambda n.c\ h\ (t\ c\ n)\\\operatorname {append} &\equiv \lambda l.\lambda t.\lambda c.\lambda n.l\ c\ (t\ c\ n)\\\operatorname {isnil} &\equiv \lambda l.l\ (\lambda h.\lambda r.\operatorname {false} )\ \operatorname {true} \\\operatorname {nonempty} &\equiv \lambda l.l\ (\lambda h.\lambda r.\operatorname {true} )\ \operatorname {false} \\\operatorname {head} &\equiv \lambda l.l\ (\lambda h.\lambda r.h)\ \operatorname {false} \\\operatorname {map} &\equiv \lambda f.\lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda r.c\ (f\ h)\ r)\ n\\\operatorname {tail} &\equiv \lambda l.\lambda c.\lambda n.l\ (\lambda h.\lambda r.\lambda g.g\ h\ (r\ c))\ (\lambda c.n)\ (\lambda h.\lambda t.t)\end{aligned}}

此列表表示可在系統F類型系統中定義。

與邱奇數的對應關係並非巧合，邱奇數本質上是單元值列表（如[() () ()]）的一進制編碼，列表長度即表示自然數值。對此類列表進行右摺疊時，組合函數忽略元素值，其本質與邱奇數中的函數組合鏈（即(c () ∘ c () ∘ c ()) n = (f ∘ f ∘ f) n）具有等價性。

Scott編碼列表表示

另一種實現方式是採用Scott編碼，這種方式能生成更簡潔的代碼^[10]（參見摩根森-斯科特編碼）。

該編碼的核心思想是利用模式匹配的特性。以Scala語法為例，假設list表示包含空列表Nil和構造器Cons(h, t)的列表類型，可通過模式匹配進行計算：

list match {
  case Nil        => nilCode
  case Cons(h, t) => consCode(h,t)
}

列表的行為由其模式匹配決定，因此可將列表定義為接收nilCode和consCode參數的函數：

\operatorname {list} \ \operatorname {nilCode} \ \operatorname {consCode}

設n對應空列表處理參數，c對應非空列表處理參數，則：空列表定義為：

\operatorname {nil} \equiv \lambda n.\lambda c.\ n

非空列表（含首元素h和尾部t）定義為：

\operatorname {cons} \ h\ t\ \ \equiv \ \ \lambda n.\lambda c.\ c\ h\ t

更一般地，包含 $m$ 種構造器的代數數據類型將被編碼為具有 $m$ 個參數的函數。當第 $i$ 個構造器包含 $n_{i}$ 個參數時，對應編碼參數也接收 $n_{i}$ 個參數。

該編碼可在無類型λ演算中使用，但帶類型版本需支持遞歸和類型多態的系統。以元素類型E、計算結果類型C的列表為例，其遞歸類型定義為（"=>"表示函數類型）：

type List =
  C =>                    // 空列表分支
  (E => List => C) =>     // 非空列表分支
  C                       // 模式匹配结果

支持任意計算類型的列表需量化類型C，而泛型列表還需將元素類型E作為類型參數。

參見

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

外部連結

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

^ ^1.0 ^1.1 ^1.2 Trancón y Widemann, Baltasar; Parnas, David Lorge. Olaf Chitil; Zoltán Horváth; Viktória Zsók , 編. Implementation and Application of Functional Languages. 19th International Workshop, IFL 2007, Freiburg, Germany, September 27–29, 2007 Revised Selected Papers. Lecture Notes in Computer Science 5083: 228–229. 2008. ISBN 978-3-540-85372-5. doi:10.1007/978-3-540-85373-2_13.
^ Jansen, Jan Martin; Koopman, Pieter W. M.; Plasmeijer, Marinus J. Efficient interpretation by transforming data types and patterns to functions. Nilsson, Henrik (編). Trends in functional programming. Volume 7. Bristol: Intellect. 2006: 73–90. CiteSeerX 10.1.1.73.9841 . ISBN 978-1-84150-188-8.
^ Predecessor and lists are not representable in simply typed lambda calculus. Lambda Calculus and Lambda Calculators. okmij.org.
^ Allison, Lloyd. Lambda Calculus Integers.
^ Bauer, Andrej. Andrej对问题的回答："使用lambda演算表示负数和复数".
^ 精确实数计算. Haskell. （原始內容存檔於2015-03-26）.
^ Bauer, Andrej. 实数计算软件. GitHub. 2022-09-26.
^ Pierce, Benjamin C. 类型与程序语言. 麻省理工出版社. 2002: 500. ISBN 978-0-262-16209-8.
^ 川普, 約翰. 14. 二元λ演算与组合逻辑. 卡魯德, 克里斯蒂安·S (編). 从莱布尼茨到柴廷的随机性与复杂性. 世界科學出版公司. 2007: 237–262. ISBN 978-981-4474-39-9.
PDF版本：川普, 約翰. 二元λ演算与组合逻辑 (PDF). 2014-05-14 [2017-11-24].
^ Jansen, Jan Martin. λ演算编程：从Church到Scott的往返. Achten, Peter; Koopman, Pieter W. M. (編). 函数式代码之美——献给里努斯·普拉斯梅尔的61岁诞辰. 計算機科學講義 8106. 施普林格. 2013: 168–180. ISBN 978-3-642-40354-5. doi:10.1007/978-3-642-40355-2_12.

[Church_numeral_definition-4] 此公式是邱奇數 $n$ 的定義，其中 $f\to b,x\to f$ 。

[ce-5] 2.0 ^2.1 在邱奇編碼中，
$\operatorname {pred} (0)=0$

$m\leq n\to m-n=0$

[3] $\operatorname {pred} (0)=0$

[4] $m\leq n\to m-n=0$

[Widemann-1] 1.0 ^1.1 ^1.2 Trancón y Widemann, Baltasar; Parnas, David Lorge. Olaf Chitil; Zoltán Horváth; Viktória Zsók , 編. Implementation and Application of Functional Languages. 19th International Workshop, IFL 2007, Freiburg, Germany, September 27–29, 2007 Revised Selected Papers. Lecture Notes in Computer Science 5083: 228–229. 2008. ISBN 978-3-540-85372-5. doi:10.1007/978-3-540-85373-2_13.

[2] Jansen, Jan Martin; Koopman, Pieter W. M.; Plasmeijer, Marinus J. Efficient interpretation by transforming data types and patterns to functions. Nilsson, Henrik (編). Trends in functional programming. Volume 7. Bristol: Intellect. 2006: 73–90. CiteSeerX 10.1.1.73.9841 . ISBN 978-1-84150-188-8.

[3] Predecessor and lists are not representable in simply typed lambda calculus. Lambda Calculus and Lambda Calculators. okmij.org.

[6] Allison, Lloyd. Lambda Calculus Integers.

[7] Bauer, Andrej. Andrej对问题的回答："使用lambda演算表示负数和复数".

[8] 精确实数计算. Haskell. （原始內容存檔於2015-03-26）.

[9] Bauer, Andrej. 实数计算软件. GitHub. 2022-09-26.

[10] Pierce, Benjamin C. 类型与程序语言. 麻省理工出版社. 2002: 500. ISBN 978-0-262-16209-8.

[11] 川普, 約翰. 14. 二元λ演算与组合逻辑. 卡魯德, 克里斯蒂安·S (編). 从莱布尼茨到柴廷的随机性与复杂性. 世界科學出版公司. 2007: 237–262. ISBN 978-981-4474-39-9.
PDF版本：川普, 約翰. 二元λ演算与组合逻辑 (PDF). 2014-05-14 [2017-11-24].

[12] Jansen, Jan Martin. λ演算编程：从Church到Scott的往返. Achten, Peter; Koopman, Pieter W. M. (編). 函数式代码之美——献给里努斯·普拉斯梅尔的61岁诞辰. 計算機科學講義 8106. 施普林格. 2013: 168–180. ISBN 978-3-642-40354-5. doi:10.1007/978-3-642-40355-2_12.

[1]

[2]

[3]

[a]

[b]

[4]

[5]

[6]

[7]

[8]

[9]

[10]

用途

邱奇數

使用邱奇數的計算

邱奇數函數一表

前驅函數推導

值容器

Inc函數

提取函數

Const容器

前驅函數的另一種解釋

前驅函數的另一種定義

除法函式

有符號數

加減運算

乘除運算

有理數與實數

換成其它表達法

邱奇布爾值

謂詞

邱奇序對

列表編碼

雙序對列表節點

單序對列表節點

右摺疊列表表示

Scott編碼列表表示

參見

外部連結