邱奇数

邱奇数为使用邱奇编码的自然数表示法，而用以表示自然数${\displaystyle n}$ 的高阶函数是个任意函数${\displaystyle f}$ 映射到它自身的n重函数复合之函数，简言之，数的“值”即等价于参数被函数包裹的次数。

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

不论邱奇数为何，其都是接受两个参数的函数。

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

就是说，自然数${\displaystyle n}$ 被表示为邱奇数n，它对于任何lambda-项F和X有着性质：

n F X =_β Fn X。

使用邱奇数的计算

在 lambda 演算中，数值函数被表示为在邱奇数上的相应函数。这些函数在大多数函数式语言中可以通过 lambda 项的直接变换来实现（服从于类型约束）。

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

plus ≡ λm.λn.λf.λx. m f (n f x)

后继函数 ${\displaystyle {\text{succ}}(n)=n+1}$  β-等价于（plus 1）。

succ ≡ λn.λf.λx. f (n f x)

乘法函数 ${\displaystyle {\text{times}}(m,n)=m\times n}$  利用了恒等式 ${\displaystyle f^{(m\times n)}=(f^{m})^{n}}$ 。

mult ≡ λm.λn.λf. n (m f)

指数函数 ${\displaystyle \exp(m,n)=m^{n}}$  由邱奇数定义直接给出。

exp ≡ λm.λn. n m

前驱函数 ${\displaystyle {\text{pred}}(n)={\begin{cases}0&{\mbox{if }}n=0,\\n-1&{\mbox{otherwise}}\end{cases}}}$  通过生成每次都应用它们的参数 g 于 f 的 ${\displaystyle n}$  重函数复合来工作；基础情况丢弃它的 f 复本并返回 x。

pred ≡ λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)

邱奇数函数一表

* 注意在邱奇编码中,

• ${\displaystyle \operatorname {pred} (0)=0}$ 
• ${\displaystyle m<n\to m-n=0}$ 

除法函式

以下列定义可实作自然数的除法

${\displaystyle n/m=\operatorname {if} \ n\geq m\ \operatorname {then} \ 1+(n-m)/m\ \operatorname {else} \ 0}$ 

计算 ${\displaystyle n}$  除以 ${\displaystyle m}$  的递回相减时，将会计算很多次的beta归约。除非以纸笔手工来做，那么多步骤倒无关紧要，
但我们不想一直重复琐碎的归约；而判别数字是否为零的函式是 IsZero，所以考虑下列条件：

${\displaystyle \operatorname {IsZero} \ (\operatorname {minus} \ n\ m)}$ 

这个判别式相当于 ${\displaystyle n}$  小于等于 ${\displaystyle m}$  而非 ${\displaystyle n}$  小于 ${\displaystyle m}$ 。如果使用这式子，那么要将上面给出的除法定义，
转化为邱奇编码的自然数函数如下，

${\displaystyle \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)}$ 

这样的定义只呼叫了一次 ${\displaystyle n}$  减去 ${\displaystyle m}$ ，正如我们所想的。然而问题是这式子计算成错误的结果，
是 (n-1)/m 除法的商。要更正则需在呼叫 divide 之前把 ${\displaystyle n}$  再加回 1。 因此除法的正确定义是，

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

divide1 是一个内含递回的定义式，要以 Y 组合子来发生递回作用。 所以要再宣告一个名为 div 的新函数；

• 等号左侧为 divide1 → div c
• 等号右侧为 divide1 → c

要获得

${\displaystyle \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)}$ 

那么

${\displaystyle \operatorname {divide} =\lambda n.\operatorname {divide1} \ (\operatorname {succ} \ n)}$ 

而式中所用的其它函式定义如下列：

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

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

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

使用倒斜线 \ 代替 λ 符号，完整的除法函式则如下列，

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

换成其它表达法

大部分真实世界的编程语言都提供原生于机器的整数，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 即为一例。

布尔逻辑可以想成二选一，而布尔值则表示为有两个参数的函数，它得到两个参数中的一个：

• 真 则选择第一个参数
• 假 则选择第二个参数

邱奇布尔值在lambda演算中的形式定义如下：

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

由于真、假 可以选择第一个或第二个参数，所以其能够由组合来产生逻辑运算子。注意到 not 版本因不同求值策略而有两个。下列为从邱奇布尔值推导来的布尔算术的函数：

${\displaystyle {\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\ ^{\scriptstyle {\text{*1}}}\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \ ^{\scriptstyle {\text{*2}}}\\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}}$ 

注：

• ¹ 求值策略使用应用次序时，这个方法才正确。
• ² 求值策略使用正常次序时，这个方法才正确。

下头为一些范例：

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

• Lambda演算
• 系统F，在有类型lambda演算中的邱奇数

• Some interactive examples of Church numerals （页面存档备份，存于互联网档案馆）

1. ^ This formula is the definition of a Church numeral n with f -> m, x -> f.