邱奇数

维基百科,自由的百科全书
跳到导航 跳到搜索

邱奇编码是把数据和运算符嵌入到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]
前驅*

減法* ...

* 注意在邱奇編碼中,

換成其它表達法[编辑]

大部分真實世界的程式語言都提供原生於機器的整數,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 求值策略使用正常次序時,這個方法才正確。


下頭為一些範例:

参见[编辑]

外部链接[编辑]

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