邱奇数

邱奇编码是把数据和运算符嵌入到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}$