[科普中國(guó)]-邱奇數(shù)

概述

邱奇編碼是把數(shù)據(jù)和運(yùn)算符嵌入到lambda演算內(nèi)的一種方式，最常見(jiàn)的形式是邱奇數(shù)，它是使用lambda符號(hào)的自然數(shù)的表示法。這種方法得名于阿隆佐·邱奇，他首先以這種方法把數(shù)據(jù)編碼到lambda演算中1。

在其他符號(hào)系統(tǒng)中通常被認(rèn)定為基本的項(xiàng)（比如整數(shù)、布爾值、有序?qū)Α⒘斜砗蛅agged unions）都被映射到使用 邱奇編碼的高階函數(shù)；根據(jù)邱奇-圖靈論題我們知道任何可計(jì)算的運(yùn)算符（和它的運(yùn)算數(shù)）都可以用邱奇編碼表示。

很多學(xué)數(shù)學(xué)的學(xué)生熟悉可計(jì)算函數(shù)集合的哥德?tīng)柧幪?hào)；邱奇編碼是定義在lambda抽象而不是自然數(shù)上的等價(jià)運(yùn)算。

Church數(shù)Church數(shù)是在Church編碼下的自然數(shù)的表示法。表示自然數(shù)n的高階函數(shù)是把任何其他函數(shù)f映射到它的n重函數(shù)復(fù)合的函數(shù)。

定義Church數(shù)0, 1, 2, ...在lambda演算中被定義如下：

0 ≡ λf.λx. x

1 ≡ λf.λx. f x

2 ≡ λf.λx. f (f x)

3 ≡ λf.λx. f (f (f x))

...

n ≡ λf.λx. fn x

...

就是說(shuō)，自然數(shù) {\displaystyle n} n被表示為Church數(shù)n，它對(duì)于任何lambda-項(xiàng)F和X有著性質(zhì)：

n F X =β Fn X。

使用Church數(shù)的計(jì)算在lambda演算中，數(shù)值函數(shù)被表示為在Church數(shù)上的相應(yīng)函數(shù)。這些函數(shù)在大多數(shù)函數(shù)式語(yǔ)言中可以通過(guò)lambda項(xiàng)的直接變換來(lái)實(shí)現(xiàn)（服從于類(lèi)型約束）。

加法函數(shù) plus(m,n)=m+n 利用了恒等式 f^{{(m+n)}}(x)=f^{m}(f^{n}(x))。

plus ≡ λm.λn.λf.λx. m f (n f x)

后繼函數(shù)succ(n)=n+1 β-等價(jià)于（plus 1）。

succ ≡ λn.λf.λx. f (n f x)

乘法函數(shù)times(m,n)=m*n利用了恒等式 f^{{(m*n)}}=(f^{m})^{n}。

mult ≡ λm.λn.λf. n (m f)

指數(shù)函數(shù) exp(m,n)=m^{n}由Church數(shù)定義直接給出。

exp ≡ λm.λn. n m

前驅(qū)函數(shù) 通過(guò)生成每次都應(yīng)用它們的參數(shù)g于f的n重函數(shù)復(fù)合來(lái)工作；基礎(chǔ)情況丟棄它的f復(fù)本并返回x。

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

Church布爾值Church布爾值是布爾值真和假的Church編碼。布爾值被表示為兩個(gè)參數(shù)的函數(shù)，它得到這兩個(gè)參數(shù)中的一個(gè)。

lambda演算中的形式定義：

true ≡ λa.λb. a

false ≡ λa.λb. b

從Church布爾值推導(dǎo)來(lái)的布爾算術(shù)的函數(shù)：

and ≡ λm.λn.λa.λb. m (n a b) b

or ≡ λm.λn.λa.λb. m a (n a b)

not ≡ λm.λa.λb. m b a