邱奇数

维基百科,自由的百科全书
跳转至: 导航搜索

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

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

很多学数学的学生熟悉可计算函数集合的哥德尔编号;邱奇编码是定义在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. fn x
...

就是说,自然数n被表示为Church数n,它对于任何lambda-项FX有着性质:

n F X =β Fn X

使用Church数的计算[编辑]

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

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

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

后继函数succ(n)=n+1 β-等价于(plus 1)。

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

乘法函数times(m,n)=m*n利用了恒等式f^{(m*n)} = (f^m)^n

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

指数函数exp(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}通过生成每次都应用它们的参数gfn重函数复合来工作;基础情况丢弃它的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

参见[编辑]

外部链接[编辑]