Church数

维基百科，自由的百科全书

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

在其他符号系统中通常被认定为基本的项(比如整数、布尔值、有序对、列表和 tagged unions)都被映射到使用 Church 编码的高阶函数；根据邱奇-图灵论题我们知道任何可计算的运算符(和它的运算数)都可以用 Church 编码表示。

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

[编辑] Church 数

Church 数是在 Church 编码下的自然数的表示法。表示自然数 $n$ 的高阶函数是把任何其他函数 $f$ 映射到它的 n 重函数复合 $f^n = f \circ f \circ \ldots \circ f$ 的函数。

[编辑] 定义

Church 数 0, 1, 2, ... 在 lambda 演算中被定义如下:

0 ≡ λf.λx. x

1 ≡ λf.λx. f x

2 ≡ λf.λx. f (f x)

3 ≡ λf.λx. f (f (f x))

...

n ≡ λf.λx. fⁿ x

...

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

n F X =_β Fⁿ X。

[编辑] 使用 Church 数的计算

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

加法函数 $p l u s (m, n) = m + n$ 利用了恒等式 $f (m + n) (x) = f m (f n (x))$ 。

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

后继函数 $s u c c (n) = n + 1$ β-等价于 (plus 1)。

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

乘法函数 $t i m e s (m, n) = m * n$ 利用了恒等式 $f (m * n) = (f m) n$ 。

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

指数函数 $e x p (m, n) = m n$ 由 Church 数定义直接给出。

exp ≡ λm.λn. n m

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

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

[编辑] Church 布尔值

Church 布尔值是布尔值真和假的 Church 编码。布尔值被表示为两个参数的函数，它得到这两个参数中的一个。

lambda 演算中的形式定义:

true ≡ λa.λb. a

false ≡ λa.λb. b

从Church 布尔值推导来的布尔算术的函数:

and ≡ λm.λn.λa.λb. m (n a b) b

or ≡ λm.λn.λa.λb. m a (n a b)

not ≡ λm.λa.λb. m b a

[编辑] 参见

Lambda 演算
系统 F，在有类型 lambda 演算中的 Church 数

[编辑] 外部链接

Some interactive examples of Church numerals

来自“http://zh.wikipedia.org../../../c/h/u/Church%E6%95%B0.html”

页面分类: 递归论