邱奇編碼是把數據和運算符嵌入到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.