邱奇編碼 是把數據和運算符嵌入到lambda演算 內的一種方式,最常見的形式即邱奇數,它使用lambda符號表示自然數。方法得名於阿隆佐·邱奇 ,他首先以這種方法把數據編碼到lambda演算中。
透過邱奇編碼,在其他符號系統中通常被認定為基本的項(比如整數、布爾值、有序對、列表和tagged unions)都會被映射到高階函數 。在無型別lambda演算 ,函數是唯一的原始型別 。
邱奇編碼本身並非用來實踐原始型別,而是透過它來展現我們不須額外原始型別即可表達計算。
很多學數學的學生熟悉可計算函數 集合的哥德爾編號 ;邱奇編碼是定義在lambda抽象 而不是自然數上的等價運算。
邱奇數
邱奇數 為使用邱奇編碼的自然數 表示法,而用以表示自然數
n
{\displaystyle n}
的高階函數 是個任意函數
f
{\displaystyle f}
映射到它自身的n 重函數複合 之函數,簡言之,數的「值」即等價於參數被函數包裹的次數。
f
∘
n
=
f
∘
f
∘
⋯
∘
f
⏟
n
次
.
{\displaystyle f^{\circ n}=\underbrace {f\circ f\circ \cdots \circ f} _{n{\text{ 次}}}.\,}
不論邱奇數為何,其都是接受兩個參數的函數。
自 然 數
函 數 定 義
lambda 表 達 式
0
0
f
x
=
x
0
=
λ
f
.
λ
x
.
x
1
1
f
x
=
f
x
1
=
λ
f
.
λ
x
.
f
x
2
2
f
x
=
f
(
f
x
)
2
=
λ
f
.
λ
x
.
f
(
f
x
)
3
3
f
x
=
f
(
f
(
f
x
)
)
3
=
λ
f
.
λ
x
.
f
(
f
(
f
x
)
)
⋮
⋮
⋮
n
n
f
x
=
f
n
x
n
=
λ
f
.
λ
x
.
f
∘
n
x
{\displaystyle {\begin{array}{r|l|l}{\text{ 自 然 數}}&{\text{函 數 定 義}}&{\text{lambda 表 達 式}}\\\hline 0&0\ f\ x=x&0=\lambda f.\lambda x.x\\1&1\ f\ x=f\ x&1=\lambda f.\lambda x.f\ x\\2&2\ f\ x=f\ (f\ x)&2=\lambda f.\lambda x.f\ (f\ x)\\3&3\ f\ x=f\ (f\ (f\ x))&3=\lambda f.\lambda x.f\ (f\ (f\ x))\\\vdots &\vdots &\vdots \\n&n\ f\ x=f^{n}\ x&n=\lambda f.\lambda x.f^{\circ n}\ x\end{array}}}
就是說,自然數
n
{\displaystyle n}
被表示為邱奇數n ,它對於任何lambda-項F
和X
有着性質:
n F X
=β Fn X
。
使用邱奇數的計算
在 lambda 演算中,數值函數被表示為在邱奇數上的相應函數。這些函數在大多數函數式語言中可以通過 lambda 項的直接變換來實現(服從於類型約束)。
加法函數
plus
(
m
,
n
)
=
m
+
n
{\displaystyle {\text{plus}}(m,n)=m+n}
利用了恆等式
f
(
m
+
n
)
(
x
)
=
f
m
(
f
n
(
x
)
)
{\displaystyle f^{(m+n)}(x)=f^{m}(f^{n}(x))}
。
plus ≡ λm.λn.λf.λx. m f (n f x)
後繼函數
succ
(
n
)
=
n
+
1
{\displaystyle {\text{succ}}(n)=n+1}
β-等價 於(plus 1 )。
succ ≡ λn.λf.λx. f (n f x)
乘法函數
times
(
m
,
n
)
=
m
×
n
{\displaystyle {\text{times}}(m,n)=m\times n}
利用了恆等式
f
(
m
×
n
)
=
(
f
m
)
n
{\displaystyle f^{(m\times n)}=(f^{m})^{n}}
。
mult ≡ λm.λn.λf. n (m f)
指數函數
exp
(
m
,
n
)
=
m
n
{\displaystyle \exp(m,n)=m^{n}}
由邱奇數定義直接給出。
exp ≡ λm.λn. n m
前驅函數
pred
(
n
)
=
{
0
if
n
=
0
,
n
−
1
otherwise
{\displaystyle {\text{pred}}(n)={\begin{cases}0&{\mbox{if }}n=0,\\n-1&{\mbox{otherwise}}\end{cases}}}
通過生成每次都應用它們的參數 g
於 f
的
n
{\displaystyle n}
重函數複合來工作;基礎情況丟棄它的 f
複本並返回 x
。
pred ≡ λn.λf.λx. n (λg.λh. h (g f)) (λu. x) (λu. u)
邱奇數函數一表
* 注意在邱奇編碼中,
pred
(
0
)
=
0
{\displaystyle \operatorname {pred} (0)=0}
m
<
n
→
m
−
n
=
0
{\displaystyle m<n\to m-n=0}
除法函式
以下列定義可實作自然數的除法
n
/
m
=
if
n
≥
m
then
1
+
(
n
−
m
)
/
m
else
0
{\displaystyle n/m=\operatorname {if} \ n\geq m\ \operatorname {then} \ 1+(n-m)/m\ \operatorname {else} \ 0}
計算
n
{\displaystyle n}
除以
m
{\displaystyle m}
的遞迴相減時,將會計算很多次的beta歸約。除非以紙筆手工來做,那麼多步驟倒無關緊要,
但我們不想一直重複瑣碎的歸約;而判別數字是否為零的函式是 IsZero,所以考慮下列條件:
IsZero
(
minus
n
m
)
{\displaystyle \operatorname {IsZero} \ (\operatorname {minus} \ n\ m)}
這個判別式相當於
n
{\displaystyle n}
小於等於
m
{\displaystyle m}
而非
n
{\displaystyle n}
小於
m
{\displaystyle m}
。如果使用這式子,那麼要將上面給出的除法定義,
轉化為邱奇編碼的自然數函數如下,
divide1
n
m
f
x
=
(
λ
d
.
IsZero
d
(
0
f
x
)
(
f
(
divide1
d
m
f
x
)
)
)
(
minus
n
m
)
{\displaystyle \operatorname {divide1} \ n\ m\ f\ x=(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (\operatorname {divide1} \ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}
這樣的定義只呼叫了一次
n
{\displaystyle n}
減去
m
{\displaystyle m}
,正如我們所想的。然而問題是這式子計算成錯誤的結果,
是 (n-1)/m 除法的商。要更正則需在呼叫 divide 之前把
n
{\displaystyle n}
再加回 1。 因此除法的正確定義是,
divide
n
=
divide1
(
succ
n
)
{\displaystyle \operatorname {divide} \ n=\operatorname {divide1} \ (\operatorname {succ} \ n)}
divide1 是一個內含遞迴的定義式,要以 Y 組合子來發生遞迴作用。 所以要再宣告一個名為 div 的新函數;
等號左側為 divide1 → div c
等號右側為 divide1 → c
要獲得
div
=
λ
c
.
λ
n
.
λ
m
.
λ
f
.
λ
x
.
(
λ
d
.
IsZero
d
(
0
f
x
)
(
f
(
c
d
m
f
x
)
)
)
(
minus
n
m
)
{\displaystyle \operatorname {div} =\lambda c.\lambda n.\lambda m.\lambda f.\lambda x.(\lambda d.\operatorname {IsZero} \ d\ (0\ f\ x)\ (f\ (c\ d\ m\ f\ x)))\ (\operatorname {minus} \ n\ m)}
那麼
divide
=
λ
n
.
divide1
(
succ
n
)
{\displaystyle \operatorname {divide} =\lambda n.\operatorname {divide1} \ (\operatorname {succ} \ n)}
而式中所用的其它函式定義如下列:
divide1
=
Y
div
succ
=
λ
n
.
λ
f
.
λ
x
.
f
(
n
f
x
)
Y
=
λ
f
.
(
λ
x
.
f
(
x
x
)
)
(
λ
x
.
f
(
x
x
)
)
0
=
λ
f
.
λ
x
.
x
IsZero
=
λ
n
.
n
(
λ
x
.
false
)
true
{\displaystyle {\begin{aligned}\operatorname {divide1} &=Y\ \operatorname {div} \\\operatorname {succ} &=\lambda n.\lambda f.\lambda x.f\ (n\ f\ x)\\Y&=\lambda f.(\lambda x.f\ (x\ x))\ (\lambda x.f\ (x\ x))\\0&=\lambda f.\lambda x.x\\\operatorname {IsZero} &=\lambda n.n\ (\lambda x.\operatorname {false} )\ \operatorname {true} \end{aligned}}}
true
≡
λ
a
.
λ
b
.
a
false
≡
λ
a
.
λ
b
.
b
{\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}
minus
=
λ
m
.
λ
n
.
n
pred
m
pred
=
λ
n
.
λ
f
.
λ
x
.
n
(
λ
g
.
λ
h
.
h
(
g
f
)
)
(
λ
u
.
x
)
(
λ
u
.
u
)
{\displaystyle {\begin{aligned}\operatorname {minus} &=\lambda m.\lambda n.n\operatorname {pred} m\\\operatorname {pred} &=\lambda n.\lambda f.\lambda x.n\ (\lambda g.\lambda h.h\ (g\ f))\ (\lambda u.x)\ (\lambda u.u)\end{aligned}}}
使用倒斜線 \ 代替 λ 符號,完整的除法函式則如下列,
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))
換成其它表達法
大部分真實世界的程式語言都提供原生於機器的整數,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演算 中的形式定義如下:
true
≡
λ
a
.
λ
b
.
a
false
≡
λ
a
.
λ
b
.
b
{\displaystyle {\begin{aligned}\operatorname {true} &\equiv \lambda a.\lambda b.a\\\operatorname {false} &\equiv \lambda a.\lambda b.b\end{aligned}}}
由於真 、假 可以選擇第一個或第二個參數,所以其能夠由組合來產生邏輯運算子。注意到 not 版本因不同求值策略 而有兩個。下列為從邱奇布爾值推導來的布爾算術的函數:
and
=
λ
p
.
λ
q
.
p
q
p
or
=
λ
p
.
λ
q
.
p
p
q
not
1
=
λ
p
.
λ
a
.
λ
b
.
p
b
a
*1
not
2
=
λ
p
.
p
(
λ
a
.
λ
b
.
b
)
(
λ
a
.
λ
b
.
a
)
=
λ
p
.
p
false
true
*2
xor
=
λ
a
.
λ
b
.
a
(
not
b
)
b
if
=
λ
p
.
λ
a
.
λ
b
.
p
a
b
{\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}}}
註:
1 求值策略使用應用次序時,這個方法才正確。
2 求值策略使用正常次序時,這個方法才正確。
下頭為一些範例:
and
true
false
=
(
λ
p
.
λ
q
.
p
q
p
)
true
false
=
true
false
true
=
(
λ
a
.
λ
b
.
a
)
false
true
=
false
or
true
false
=
(
λ
p
.
λ
q
.
p
p
q
)
(
λ
a
.
λ
b
.
a
)
(
λ
a
.
λ
b
.
b
)
=
(
λ
a
.
λ
b
.
a
)
(
λ
a
.
λ
b
.
a
)
(
λ
a
.
λ
b
.
b
)
=
(
λ
a
.
λ
b
.
a
)
=
true
not
1
true
=
(
λ
p
.
λ
a
.
λ
b
.
p
b
a
)
(
λ
a
.
λ
b
.
a
)
=
λ
a
.
λ
b
.
(
λ
a
.
λ
b
.
a
)
b
a
=
λ
a
.
λ
b
.
(
λ
c
.
b
)
a
=
λ
a
.
λ
b
.
b
=
false
not
2
true
=
(
λ
p
.
p
(
λ
a
.
λ
b
.
b
)
(
λ
a
.
λ
b
.
a
)
)
(
λ
a
.
λ
b
.
a
)
=
(
λ
a
.
λ
b
.
a
)
(
λ
a
.
λ
b
.
b
)
(
λ
a
.
λ
b
.
a
)
=
(
λ
b
.
(
λ
a
.
λ
b
.
b
)
)
(
λ
a
.
λ
b
.
a
)
=
λ
a
.
λ
b
.
b
=
false
{\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}}}
參見
外部連結
^ This formula is the definition of a Church numeral n with f -> m, x -> f.