邱奇编码是把数据和运算符嵌入到lambda演算内的一种方式,最常见的形式即邱奇数,它使用lambda符号表示自然数。方法得名于阿隆佐·邱奇,他首先以这种方法把数据编码到lambda演算中。
透过邱奇编码,在其他符号系统中通常被认定为基本的项(比如整数、布尔值、有序对、列表和tagged unions)都会被映射到高阶函数。在无型别lambda演算,函数是唯一的原始型别。
邱奇编码本身并非用来实践原始型别,而是透过它来展现我们不须额外原始型别即可表达计算。
很多学数学的学生熟悉可计算函数集合的哥德尔编号;邱奇编码是定义在lambda抽象而不是自然数上的等价运算。
在 lambda 演算中,数值函数被表示为在邱奇数上的相应函数。这些函数在大多数函数式语言中可以通过 lambda 项的直接变换来实现(服从于类型约束)。
加法函数 利用了恒等式 。
- plus ≡
λm.λn.λf.λx. m f (n f x)
后继函数 β-等价于(plus 1)。
- succ ≡
λn.λf.λx. f (n f x)
乘法函数 利用了恒等式 。
- mult ≡
λm.λn.λf. n (m f)
指数函数 由邱奇数定义直接给出。
- exp ≡
λm.λn. n m
前驱函数 通过生成每次都应用它们的参数 g
于 f
的 重函数复合来工作;基础情况丢弃它的 f
复本并返回 x
。
- pred ≡
λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)
More information , ... Close
* 注意在邱奇编码中,
大部分真实世界的编程语言都提供原生于机器的整数,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演算中的形式定义如下:
由于真、假 可以选择第一个或第二个参数,所以其能够由组合来产生逻辑运算子。注意到 not 版本因不同求值策略而有两个。下列为从邱奇布尔值推导来的布尔算术的函数:
注:
- 1 求值策略使用应用次序时,这个方法才正确。
- 2 求值策略使用正常次序时,这个方法才正确。
下头为一些范例:
This formula is the definition of a Church numeral n with f -> m, x -> f.