無類型Lambda演算筆記-2（Lambda可定義性，附Haskell實例）

01-30

目錄：類型論驛站寫作計劃

前一篇：無類型Lambda演算筆記-1（附Haskell實例）

後一篇：無類型Lambda演算筆記-3（歸約和Church-Rosser定理）

2. Lambda可定義性

Church數

定義：

當 $nin mathbb{N}$ , 且 $F,MinLambda$ 時， $F^n(M)$ 定義如下：

$F^0(M)equiv M; F^{n+1} equiv F(F^n(M))$

2. Church數 $textbf{c}_0, textbf{c}_1,textbf{c}_2,...$ 定義如下：

$textbf{c}_n equiv lambda fx.f^n(x).$

Haskell實例：

"Prelude:" ling = s z -> z -- 定義 0nling :: t1 -> t -> t --如果不能自動顯示類型，可以用:set +t來設定；消除類型顯示用:unset +t來設定 n"Prelude:" yi = s z -> s z -- 定義 1nyi :: (t1 -> t) -> t1 -> tnn"Prelude:" xianshi n = n (1+) 0 --定義「顯示」，方便核對我們定義的正確性nxianshi :: (Num t, Num a) => ((a -> a) -> t -> t1) -> t1n"Prelude:" xianshi ling -- 顯示 0n0nit :: Num t1 => t1n"Prelude:" xianshi yi -- 顯示 1n1nit :: Num t1 => t1n"Prelude:" er = s z -> s (s z) --定義2ner :: (t -> t) -> t -> tn"Prelude:" xianshi er -- 顯示 2n2nit :: Num t1 => t1nn-- 定義後繼n"Prelude:" houji n s = n s . snhouji :: ((a -> b) -> b -> c) -> (a -> b) -> a -> cn"Prelude:" yi = houji ling -- 使用後繼定義 1nyi :: (a -> c) -> a -> cn"Prelude:" xianshi yi -- 顯示 1n1nit :: Num t1 => t1nn"Prelude:" :t (.) -- (.) 是複合函數（funciton composition）的組合子n(.) :: (b -> c) -> (a -> b) -> a -> cn

J. B. Rosser 命題

定義：

$textbf{A}_+ equiv lambda xypq.xp(ypq); textbf{A}_* equiv lambda x y z.x(yz); textbf{A}_{exp} equiv lambda xy.yx.$

那麼對於所有 $n,minmathbb{N}$ ，我們有：

$1. textbf{A}_+c_nc_m = c_{n+m}. 2. textbf{A}_*c_n c_m = c_{nm}. 3. textbf{A}_{exp}c_nc_m = c_{(n^m)}, 除非m = 0.$

引理1

$1. (c_nx)^m (y)= x^{n*m}(y); 2. (c_n)^m(x)=c_{(n^m)}(x), 對於m>0.$

引理1的證明

用歸納法。若 $m$ 為0，則 $(c_nx)^m (y) =y= x^{n*m}(y)$ . 若(1)對於 $m$ 成立，那麼

$(c_nx)^{m+1}(y) = c_nx((c_nx)^m(y)) hspace{6.1cm} =c_nx(x^{n*m}(y)) hspace{1cm} text{Induction Hypothesis} =x^{n*1}(x^{n*m}(y)) hspace{4.3cm} =x^n(x^{n*m}(y)) hspace{4.5cm} =x^{n+n*m}(y)hspace{4.8cm} =x^{n*(m+1)}(y).hspace{4.5cm}$

2. 用歸納法，以 $m=1$ 為基礎，易證。

Rosser命題的證明

對於 $m$ 使用使用歸納法。
使用引理1（1）.
由引理1（2），可知對於 $m>0,$

$textbf{A}_{exp}textbf{c}_ntextbf{c}_m=textbf{c}_mtextbf{c}_n=lambda x.{c_n}^m(x) =lambda x.c_{(n^m)} = c_{(n^m)}.$

Haskell實例：

"Prelude:" jia = n m s z -> n s (m s z) -- 定義加法算術運算njia :: (t3 -> t2 -> t1) -> (t3 -> t -> t2) -> t3 -> t -> t1n"Prelude:" er = jia yi yi -- 使用 1+1定義2ner :: (a -> a) -> a -> ann"Prelude:" cheng = x y z -> x (y z) --定義乘法ncheng :: (t2 -> t1) -> (t -> t2) -> t -> t1n"敕 Prelude:" si = cheng er er --使用2*2定義4nsi :: (a -> a) -> a -> an"Prelude:" xianshi sin4nit :: Num t1 => t1nn"Prelude:" zhishu = x y -> y x --定義指數nzhishu :: t1 -> (t1 -> t) -> tn"Prelude:" xianshi (zhishu er san) -- 顯示「二的三次方」n8nit :: Num t1 => t1n"Prelude:" xianshi (zhishu shi er)n"Prelude:" shi = jia (zhishu er san) er --定義10nshi :: (t1 -> t1) -> t1 -> t1n"Prelude:" xianshi shin10nit :: Num t1 => t1n"Prelude:" xianshi (zhishu shi er) --顯示「十的二次方」n100nit :: Num t1 => t1n

布爾值，條件式（Booleans and conditional）的定義

$textbf{true} equiv lambda xy.x textbf{false} equiv lambda xy.y$
如果 $B$ 為一個布爾項，即它或為真，或為假。那麼

$如果B則P，否則Q$

可以表示為 $BPQ$ 。

布爾值和部分布爾運算定義的Haskell演示：

"Prelude:" type CB a = a -> a -> a --定義Church Boolean類型n"Prelude:" :{ -- 定義「真假」nPrelude| zhen, jia :: CB anPrelude| zhen = x y -> xnPrelude| jia = x y -> ynPrelude| :}nn"Prelude:" :{ --顯示「真假」nPrelude| xianshiB :: CB Integer -> IntegernPrelude| xianshiB = f -> f 1 0nPrelude| :}n"Prelude:" xianshiB zhenn1n"Prelude:" xianshiB jian0nn"Prelude:" :{ --定義「不」nPrelude| bu :: CB (CB a) -> CB anPrelude| bu f = f jia zhennPrelude| :}nn"Prelude:" buzhen = bu zhen --「不」的運算演示n"Prelude:" xianshiB buzhenn0n"Prelude:" bubuzhen = bu (bu zhen)n"Prelude:" xianshiB bubuzhenn1nn"Prelude:" :{ --定義「合取」nPrelude| hequ :: CB (CB a) -> CB a -> CB anPrelude| hequ f g = f g jianPrelude| :}n"Prelude:" xianshiB (hequ zhen jia) --「合取」演示n0n"Prelude:" xianshiB (hequ zhen zhen)n1nnn"Prelude:" :{ --定義「析取」nPrelude| xiqu :: CB (CB a) -> CB a -> CB anPrelude| xiqu f g = f zhen gnPrelude| :}n"Prelude:" xianshiB (xiqu zhen jia) --「析取」演示n1n"Prelude:" xianshiB (xiqu jia jia)n0n"Prelude:" xianshiB (xiqu zhen zhen)n1n

配對（Pairing）定義

對於 $M,Nin Lambda$ ，若標記

$[M,N] equiv lambda z.z MN$

則有

$[M,N] textbf{true} = M [M,N] textbf{false} = N$

因而 $[M,N]$ 可以視為一個有序對子。

數值函數（numeric function）和 $lambda$ 可定義性（ $lambda$ -definability）的定義

數值函數是對於一個 $p$ 的一個映射 $f: mathbb{N}^p rightarrow mathbb{N}$ .
對於一個參數（arguments）數目為 $p$ 的數值函數 $f$ 來說，如果對於所有 $n_1,...,n_pin mathbb{N}$ ，對於某個組合子 $F$ ，我們有 $Ftextbf{c}_{n_1}...textbf{c}_{n_p} = textbf{c}_{f(n_1,...n_p)}$ ，那麼我們稱 $f$ 是 $lambda$ 可定義（ $lambda$ -definable）的。如果上述等式存在，那麼我們稱 $f$ 由組合子 $F$ 定義。

初始函數（initial function）和最小值 $mu$ 的定義

$U^i_r(x_1,...,x_r)=x_i, hspace{1cm}1leq i leq r; S^+(n) = n +1; hspace{0.8cm} Z (n) = 0. hspace{1.2cm}$
設 $P(n)$ 為數值關係，那麼 $mu m.P(m)$ 則表示使得 $P(m)$ 成立的最小取值。如果 $P(m)$ 永遠不成立，則不存在 $mu.$

回顧：我們在用Haskell定義Church數的時候已經用到了初始函數。

"Prelude:" ling = s z -> z -- 使用Z和S^+定義 0（但沒有給出Z和S^+的定義）nling :: t1 -> t -> t n"Prelude:" yi = s z -> s z -- 使用Z和S^+定義 1nyi :: (t1 -> t) -> t1 -> tn"Prelude:" xianshi n = n (1+) 0 --定義初始函數Z和S^+n

引理2

初始函數都是 $lambda$ 可定義的。

引理2的證明

通過Church數的定義易證。

引理3

$lambda$ 可定義的函數在函數複合（composition）下是閉合（closed）的。

引理3的證明

設函數 $g, h_1,...,h_m$ 是由組合子 $G,H_1,...,H_m$ 定義的，那麼

$f(vec{n}) = g(h_1(vec{n}),...h_m(vec{n}))$ 由 $Fequiv lambda vec{x}.G(H_1vec{x})...(H_mvec{x})$ $lambda$ 定義的。

引理4

$lambda$ 可定義函數在原始遞歸（primitive recursion）下是閉合的。

引理4的證明

設 $g,h$ 分別由 $G,H$ 實現 $lambda$ 定義，我們定義函數 $f$ 如下：

$f(0,vec{n}) = g(vec{n}) f(k+1,vec{n})=h(f(k,vec{n}),k,vec{n})$

為方便起見，先考慮 $G=textbf{c}_{f(0)}$ ，即 $vec{n}$ 不存在（若 $vec{n}$ 存在，本證明可以進行簡單的推廣）。

如果 $k$ 不是 $h$ 的參數，那麼我們就有了迭代（iteration）。由於Church數是迭代子（iterators，或譯作迭代器），我們可以用 $lambda$ 演算來便捷地表示迭代。

考慮

$Tequiv lambda p.[textsf{S}^+(ptextbf{true}, H(ptextbf{false}),(p(textbf{true})].$

則對於所有 $k$ ，我們有

$T(textbf{c}_k,textbf{c}_{f(k)}) = [ftextsf{S}^+textbf{c}_k, Htextbf{c}_{f(k)}textbf{c}_k] = [textbf{c}_{k+1},textbf{c}_{f(k+1)}].$

通過歸納 $k$ ，可得

$[textbf{c}_k,textbf{c}_{f(k)}] = T^k(textbf{c}_0,textbf{c}_{f(0)}).$

故有

$textbf{c}_{f(x)}=textbf{c}_kT[textbf{c}_0,textbf{c}_{f(0)}]textbf{false}$

從而， $f$ 可以通過組合子 $F$ 實現 $lambda$ 定義， $F$ 定義為

$Fequivlambda k.kT[textbf{c}_0, G]textbf{false}.$

證畢。

引理5

$lambda$ 可定義的函數在最小值化（minimalization）下是封閉的。

引理5的證明

我們將 $f$ 定義為 $f(vec{n}) = mu m[g(vec{n},m) = 0]$ ，其中 $vec{n} = n_1,...,n_k$ 且 $g$ 是由 $G$ 進行 $lambda$ 定義的。定義

$textbf{zero}equiv lambda n.n(textbf{true false})textbf{true}$

則有

$textbf{zero c}_0 = textbf{true}, textbf{zero c}_{n+1} = textbf{false}.$

由不動點定理引論（見上篇）可知存在一個項 $H$ ，使得

$Hvec{n}y=textbf{if} (textbf{zero}(Gvec{n}y)) textbf{then} y textbf{else} Hvec{n}(textsf{S}^+y).$

那麼 $F=lambda vec{n}.Hvec{x}textbf{c}_0$ 就可以定義 $f$ .

遞歸函數的 $lambda$ 可定義性定理

所有遞歸函數都是 $lambda$ 可定義的。（ $lambda$ 可定義函數都是遞歸函數）

遞歸函數的 $lambda$ 可定義性定理

通過引理2-5易證。

自然數的遞歸配對定義

$v^{0} = v; v^{n+1} = v^{(n)}phantom{}$ .
$sharp(v^{(n)}) = langle 0,nrangle; sharp(MN) = langle 2, langle sharp(M), sharp(N)rangle rangle; sharp(lambda x.M) = langle 3, langle sharp(x), sharp(M)rangle rangle;$
$^lceil M ^rceil = textbf{c}_{sharp M}.$

定義

設 $mathcal{A} subseteq Lambda.$

$mathcal{A}$ 在 $=$ 下是閉合的，如果 $Minmathcal{A}, lambda vdash M= N Rightarrow N in mathcal{A}.$
如果 $mathcal{A} neq varnothing, mathcal{A} neq Lambda$ ，則稱 $mathcal{A}$ 是非平凡的（non
-trivial）。
如果 $sharp mathcal{A} = {sharp M mid Min mathcal{A}}$ 是遞歸的，那麼 $mathcal{A}$ 是遞歸的（recursive）。