邱奇数

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

参见

外部链接