邱奇數

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

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

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

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

用途

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

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

邱奇數

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

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

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

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

${\displaystyle {\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的本質是函數的應用次數，而非計算結果本身。其核心意義在於「重複三次」的動作，這正是「三次」概念的直觀體現。

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

n F X =_β Fn X。

使用邱奇數的計算

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

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

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

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

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

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

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

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

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

對應的lambda表達式為：

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

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

${\displaystyle \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的容器來實現，該容器以省略第一次函數應用的方式初始化（詳見前驅函數推導）。

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

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