邱奇数

邱奇编码是把数据和运算符嵌入到lambda演算内的一种方式，最常见的形式即邱奇数，它使用lambda符号表示自然数。方法得名于阿隆佐·邱奇，他首先以这种方法把数据编码到lambda演算中。

透過邱奇編碼，在其他符号系统中通常被认定为基本的项（比如整数、布尔值、有序对、列表和tagged unions）都會被映射到高阶函数。在無型別lambda演算，函數是唯一的原始型別。

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

很多学数学的学生熟悉可计算函数集合的哥德尔编号；邱奇编码是定义在lambda抽象而不是自然数上的等价运算。

用途
直接实现邱奇编码会将某些访问操作的时间复杂度从O(1)降低到O(n)（其中n是数据结构的大小），这使得该编码方式在实际应用中受到限制。研究表明可以通过针对性优化解决这个问题，但大多数函数式编程语言选择扩展其中间表示以包含代数数据类型。
尽管如此，邱奇编码仍常用于理论论证，因为它在部分求值和定理证明中具有自然表示优势。并能便捷地实现原始递归。

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

计算n-m需要多次beta归约。除非手动进行归约，否则这并不重要，但最好避免重复计算。最简单的数值检测谓词是IsZero，故考虑条件：
: \operatorname{IsZero}\ (\operatorname{minus}\ n\ m)
此条件等价于 n \le m 而非 n。若采用该条件，则上述数学定义可转化为邱奇数函数：
: \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{align}
\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{align}
:: \begin{align}
\operatorname{true} &\equiv \lambda a.\lambda b.a\\
\operatorname{false} &\equiv \lambda a.\lambda b.b
\end{align}
: \begin{align}
\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{align}

最终展开式：
: \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)))

有符号数
通过使用包含正负值的邱奇序对，可将邱奇数扩展至有符号数。整数值即两个邱奇数的差值。

自然数转有符号数的定义为：
:\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)))

乘除运算
乘法定义为：
:xy = (x_py_p + x_ny_n) - (x_py_n + x_ny_p) = [x_py_p + x_ny_n, x_py_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)))

有理数与实数
有理数可表示为有符号数序对，可计算实数可通过极限过程编码。复数可自然地表示为实数序对。上述数据类型验证了邱奇-图灵论题：任何数据类型或计算均可编码于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和即為典型示例。

布爾邏輯本質上是選擇機制。邱奇布尔值的编码形式为接收两个参数的函数：

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

其标准定义为：
: \begin{align}
\operatorname{true} &\equiv \lambda a.\lambda b.a\\
\operatorname{false} &\equiv \lambda a.\lambda b.b
\end{align}

这种编码允许谓词函数（返回逻辑值的函数）直接作为条件语句使用。当布尔函数作用于两个参数时，将根据真值返回其中一个参数：
: \operatorname{predicate-}x\ \operatorname{then-clause}\ \operatorname{else-clause}
若predicate-x为真则返回then-clause，否则返回else-clause。

由于真值与假值的选择特性，它们可组合出各类逻辑运算符。需注意逻辑非not存在多种实现方式：
: \begin{align}
\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{align}

註：
*1 求值策略使用應用次序時，這個方法才正確。
*2 求值策略使用正常次序時，這個方法才正確。

运算示例解析：

: \begin{align}

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

谓词
谓词是返回布尔值的函数。最基础的谓词是\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 \le y \land y \le x)
相等性检测可定义为：
: \operatorname{EQ} = \lambda m.\lambda n.\operatorname{and}\ (\operatorname{LEQ}\ m\ n)\ (\operatorname{LEQ}\ n\ m)

邱奇序对
邱奇序对是二元组的邱奇编码实现。序对被表示为接收函数的函数，当传入参数时会将该参数作用于序对的两个分量。其lambda演算定义为：

: \begin{align}
\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{align}

示例推导：
: \begin{align}
& \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{align}

列表编码
不可变的列表由列表节点构成，其基本操作包括：

以下给出四种不同的列表表示法：

• 使用双序对构造列表节点（支持空列表）
• 使用单序对构造列表节点
• 基于右折叠函数的列表表示
• 采用Scott编码的模式匹配参数化表示

双序对列表节点
非空列表可用邱奇序对表示：

• First 存储首元素
• Second 存储尾部

为支持空列表，需额外包裹序对形成三层结构：

• First - 空列表标识符
• Second.First 存储首元素
• Second.Second 存储尾部

基于此的核心操作定义如下：

注意：当列表为空时，head和tail函数不应被调用。

单序对列表节点
另一种定义方式：
: \begin{align}
\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{align}

通用处理模板定义为：
: \begin{align}
\operatorname{process-list} &\equiv \lambda l.l (\lambda h.\lambda t.\lambda d. \operatorname{head-and-tail-clause}) \operatorname{nil-clause} \\
\end{align}

其他扩展操作：
: \begin{align}

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

: \begin{align}

\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{align}
----
: \begin{align}

\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{align}
----
: \begin{align}

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

右折叠列表表示
作为邱奇序对编码的替代方案，列表可通过其右折叠函数进行编码。例如，包含三个元素x、y、z的列表可编码为高阶函数，当该函数应用组合子c和初始值n时，返回c x (c y (c z n))。这等价于部分应用函数组合链的调用：(c x ∘ c y ∘ c z) n。

:
\begin{align}
\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{align}

此列表表示可在系统F类型系统中定义。

与邱奇数的对应关系并非巧合，邱奇数本质上是单元值列表（如[() () ()]）的一进制编码，列表长度即表示自然数值。对此类列表进行右折叠时，组合函数忽略元素值，其本质与邱奇数中的函数组合链（即(c () ∘ c () ∘ c ()) n = (f ∘ f ∘ f) n）具有等价性。

Scott编码列表表示
另一种实现方式是采用了续体的Scott编码，这种方式能生成更简洁的代码（参见）。

该编码的核心思想是利用模式匹配的特性。以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演算中的邱奇数

引用
外部链接
*[http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Examples/const-int/ Some interactive examples of Church numerals]