邱奇數

邱奇編碼是把數據和運算符嵌入到lambda演算內的一種方式，最常見的形式是邱奇數，它是使用lambda符號的自然數的表示法。這種方法得名於阿隆佐·邱奇，他首先以這種方法把數據編碼到lambda演算中 ^[1]  。

在其他符號系統中通常被認定為基本的項（比如整數、布爾值、有序對、列表和tagged unions）都被映射到使用 邱奇編碼的高階函數；根據邱奇-圖靈論題我們知道任何可計算的運算符（和它的運算數）都可以用邱奇編碼表示。

很多學數學的學生熟悉可計算函數集合的哥德爾編號；邱奇編碼是定義在lambda抽象而不是自然數上的等價運算。

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

Church數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

...

就是説，自然數 {\displaystyle n} n被表示為Church數n，它對於任何lambda-項F和X有着性質：

n F X =β Fn X。

在lambda演算中，數值函數被表示為在Church數上的相應函數。這些函數在大多數函數式語言中可以通過lambda項的直接變換來實現（服從於類型約束）。

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

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

後繼函數succ(n)=n+1 β-等價於（plus 1）。

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

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

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

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

exp ≡ λm.λn. n m

前驅函數 通過生成每次都應用它們的參數g於f的n重函數複合來工作；基礎情況丟棄它的f複本並返回x。

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

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

lambda演算中的形式定義：

true ≡ λa.λb. a

false ≡ λa.λb. b

從Church布爾值推導來的布爾算術的函數：

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