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

透过邱奇编码,在其他符号系统中通常被认定为基本的项(比如整数、布尔值、有序对、列表和tagged unions)都会被映射到高阶函数。在无型别lambda演算,函数是唯一的原始型别

邱奇编码本身并非用来实践原始型别,而是透过它来展现我们不须额外原始型别即可表达计算。

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

邱奇数

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

 

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

 

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

n F X =β Fn X

使用邱奇数的计算

在 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

前驱函数   通过生成每次都应用它们的参数 gf  重函数复合来工作;基础情况丢弃它的 f 复本并返回 x

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

邱奇数函数一表

函数 代数 等同 函数定义 Lambda 表达式
后继         ...
加法          
乘法          
指数    [1]      
前驱*      

 

减法*       ...  

* 注意在邱奇编码中,

  •  
  •  


除法函式

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

 


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

 


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

 


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

 


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

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


要获得

 


那么

 


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

 
 
 


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

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


换成其它表达法

大部分真实世界的编程语言都提供原生于机器的整数,churchunchurch 函式会在整数及与之对应的邱奇数间转换。这里使用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 求值策略使用正常次序时,这个方法才正确。


下头为一些范例:

 

参见

外部链接

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