邱奇編碼是把數據和運算符嵌入到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
* 注意在邱奇編碼中,
![{\displaystyle \operatorname {pred} (0)=0}](//wikimedia.org/api/rest_v1/media/math/render/svg/97760225e16261b4333c6e317dfbb6a3ee1270af)
![{\displaystyle m<n\to m-n=0}](//wikimedia.org/api/rest_v1/media/math/render/svg/111e869458320ac2efc51b8ded0ff6b33c6cc6e4)
大部分真實世界的程式語言都提供原生於機器的整數,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演算中的形式定義如下:
![{\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}](//wikimedia.org/api/rest_v1/media/math/render/svg/d39bc19720586d643dd1923cd9e054b1614725f9)
由於真、假 可以選擇第一個或第二個參數,所以其能夠由組合來產生邏輯運算子。注意到 not 版本因不同求值策略而有兩個。下列為從邱奇布爾值推導來的布爾算術的函數:
![{\displaystyle {\begin{aligned}\operatorname {and} &=\lambda p.\lambda q.p\ q\ p\\\operatorname {or} &=\lambda p.\lambda q.p\ p\ q\\\operatorname {not} _{1}&=\lambda p.\lambda a.\lambda b.p\ b\ a\ ^{\scriptstyle {\text{*1}}}\\\operatorname {not} _{2}&=\lambda p.p\ (\lambda a.\lambda b.b)\ (\lambda a.\lambda b.a)=\lambda p.p\operatorname {false} \operatorname {true} \ ^{\scriptstyle {\text{*2}}}\\\operatorname {xor} &=\lambda a.\lambda b.a\ (\operatorname {not} \ b)\ b\\\operatorname {if} &=\lambda p.\lambda a.\lambda b.p\ a\ b\end{aligned}}}](//wikimedia.org/api/rest_v1/media/math/render/svg/1877d35701daaa16e1bdcff403edd3176f941ebe)
註:
- 1 求值策略使用應用次序時,這個方法才正確。
- 2 求值策略使用正常次序時,這個方法才正確。
下頭為一些範例:
![{\displaystyle {\begin{aligned}\operatorname {and} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ q\ p)\ \operatorname {true} \ \operatorname {false} =\operatorname {true} \operatorname {false} \operatorname {true} =(\lambda a.\lambda b.a)\operatorname {false} \operatorname {true} =\operatorname {false} \\\operatorname {or} \operatorname {true} \operatorname {false} &=(\lambda p.\lambda q.p\ p\ q)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)\ (\lambda a.\lambda b.a)\ (\lambda a.\lambda b.b)=(\lambda a.\lambda b.a)=\operatorname {true} \\\operatorname {not} _{1}\ \operatorname {true} &=(\lambda p.\lambda a.\lambda b.p\ b\ a)(\lambda a.\lambda b.a)=\lambda a.\lambda b.(\lambda a.\lambda b.a)\ b\ a=\lambda a.\lambda b.(\lambda c.b)\ a=\lambda a.\lambda b.b=\operatorname {false} \\\operatorname {not} _{2}\ \operatorname {true} &=(\lambda p.p\ (\lambda a.\lambda b.b)(\lambda a.\lambda b.a))(\lambda a.\lambda b.a)=(\lambda a.\lambda b.a)(\lambda a.\lambda b.b)(\lambda a.\lambda b.a)=(\lambda b.(\lambda a.\lambda b.b))\ (\lambda a.\lambda b.a)=\lambda a.\lambda b.b=\operatorname {false} \end{aligned}}}](//wikimedia.org/api/rest_v1/media/math/render/svg/a36161f4e76c5ef328c080d27810bb395713209e)
This formula is the definition of a Church numeral n with f -> m, x -> f.