計算理論(3)

08-14

計算理論(3)

一、前情提要

在前面兩節中，我們有介紹什麼是 $lambda-calculus$ ，並在第二節中發展了一個形式推理系統 $lambda eta eta$ ，簡單描述了一下在這個形式推理系統中，能夠做到哪些事情。當然這些基於定義的簡單描述顯然不夠，這一節我們將主要介紹不動點組合子。有了不動點組合子，我們就能夠完成包括條件分支，循環，遞歸等這些命令式程序裡面的程序結構。

二、實例研究

在實際開始我們的主要理論之前，我們首先來研究一個簡單的例子。這是一個關於遞歸的例子，採用斐波那契數列。

斐波那契數列定義如下：

$F_n=left {egin{array} {ll} 1 ,& n=1,2 \ F_{n-1}+F_{n-2}, & otherwise end{array} ight.$

編寫代碼如下：

1.def fib(n):2. if n<3 :3. return 14. else:5. return (fib(n-1)+fib(n-2))

這是一個很簡單的程序。如果要在 $lambda-calculus$ 中表示出來，那麼我們首先需要一個 $if-then-else$ 這樣的分支結構，其次，因為在上面的程序中我們看到了調用的遞歸函數是使用 $fib$ 這樣的函數名字，可是在 $lambda-calculus$ 中所有函數都是匿名的（前一節給的組合子前面的名字I K S等都是符號助記），也就是說如果要調用一個函數，必須有完整的函數定義，這樣自己調用自己情況就必須另外想辦法了。現在我們知道這個辦法就是藉助不動點組合子。

三、不動點組合子

首先我們我們來看一下，如何一般地解決上述遞歸調用的問題。

先定義 $if-then-else$ 結構出來。記

$left{egin{array}{l} true=K \ false=K^* end{array} ight.$

並令 $[M,N]=lambda x.xMN$ ,則有： $[M,N]true=M,[M,N]false=N$ 。

以上說明了分支結構是 $lambda$ 可定義的。在涉及自然數時，還需要使用Church-number對自然數進行編碼，這部分暫時不做介紹。由於在普通的編程語言中都有更方便的自然數和 $if-then-else$ 結構可供使用，這裡我們就不詳細介紹如何對不同情況進行適當的編碼，也不會在之後的介紹中使用專門的編碼，而是假設我們有了一般意義上的 $if-then-else$ 結構，這裡給的示例僅作了解之用。

因此我們的斐波那契 $lambda$ 函數可以定義為

$egin{align} fib x &=if x<3 then 1 else fib (x-1) +(fib (x-2)) \ Longrightarrow fib &= lambda x.if x<3 then 1 else fib (x-1) +(fib (x-2)) end{align}$

這樣的話，在上面的 $fib$ 定義中，我們還用到 $fib$ 這樣顯示定義，現在我們把 $fib$ 抽象出來就是

$egin{align} fib &= (lambda fx.if x<3 then 1 else f (x-1) +(f (x-2))) fib end{align} ag{3.1}$

這個樣子看起來還是沒辦法用的樣子，不過這也基本讓我們看出來了如果要構造可以使用的遞歸結構應該是什麼樣子的。

令 $Fequiv egin{align} fib &= lambda fx.if x<3 then 1 else f f (x-1) +(f f (x-2)) end{align}$ ,

上面給 $fib$ 增加了一個助記符 $F$ ，對於3.1公式 $fib$ 裡面的定義，把 $f$ 換成了 $f f$ 。

Example 4. $(1) quad F F 3=2\ (2) quad F F 4=3$

驗證從略。

藉助這樣的方法，我們已經實現了遞歸。但是看起來還是很麻煩，Haskell B. Curry大神就發現了一個通用的辦法，叫做 $Y$ 不動點組合子。

Lemma 4. （不動點定理）存在 $Z in Lambda$ ,使得對於任意的 $F in Lambda$ ,有 $F Z=Z$ 。

與直覺相反，在公式3.1裡面， $fib$ 不是我們想定義的函數本身，而是前面的一串長長的。對於任意一個遞歸定義的函數 $F$ ，我們都可以找到一個合適的不動點 $Z$ ，使得 $F Z=Z$ 。從而由形式推理系統，可得 $F (F Z)=F Z =Z$ ,可得到 $F$ 的任意次應用，最後結果依然是 $Z$ ，那這樣的不動點結構是什麼樣子的呢？

Proof. 令 $W=lambda x.F(xx)$ ，取 $Z=WW=(lambda x.F(xx))W=F(WW)=Z$ 。 $Box$

對於每一個具體的 $F$ 都可以確定其不動點了,更進一步的，類似於公式3.1，抽象出 $F$ ，定義 $Y=lambda f.(lambda x.f(xx))(lambda x.f(xx))$ ，對於定理4中，有 $YF=WW=F（WW）=F（YF）$ ，這樣就容易看出來一個 $F$ 的不動點就是 $YF$ 了。

Example 5. (1)構建 $fib$ 函數的 $lambda-$ 函數。

（2）證明 $exists G forall Xquad GX=SGX$ 。

Resolution.

(1).令 $egin{align} fib = Y (lambda fx.if x<3 then 1 else f (x-1) +(f (x-2))) end{align}$ 即可。

(2).

$egin{align} forall X exists GX=SGX &Leftarrow Gx =SGx \ &Leftarrow G=lambda x.SGx \ &Leftarrow G=(lambda gx.Sgx)G \ &Leftarrow G=Y(lambda gx.Sgx). end{align}$

$ag*{$Box$}$

Lemma 5. 對於任何 $ZinLambda$ ,存在 $FinLambda$ ,使得 $FZ=F$ 。

Proof.

$egin{align} forall Z.FZ=F &Leftarrow F=lambda x.F \ & Leftarrow F=(lambda fx.f)F \ & Leftarrow Fequiv Y(lambda fx.f) end{align}$

$egin{array}{r} ag*{$Box$} end{array}$

四、多元不動點

Definition 11.令(1) $[M_1,M_2,cdots,M_n]_i equiv lambda z.zM_1M_2 cdots M_n$

(2) $([M_1,M_2 ,cdots ,M_n])_i equiv [M_1,M_2 ,cdots, M_n]U_i^n=M_i$

其中 $U_i^n=lambda x_1x_2cdots x_n.x_i$ 是序列的投影函數。

Lemma 6. 設任意的 $F_1,F_2cdots F_n in Lambda$ ,則存在 $M_1,M_2cdots M_n in Lambda$ ,使得

$egin{align} M_1=F_1M_1&M_2cdots M_n,\ M_2=F_2M_1&M_2cdots M_n,\ &vdots \ M_n=F_nM_1&M_2cdots M_n end{align}$

。

Proof.取 $M=[M_1,M_2,cdots ,M_n]$ ,

即有 $M_i=([M_1,M_2,cdots,M_n])_i=(M)_i$

從而有： $egin{align} M&=[M_1,M_2,cdots,M_n]\ &=[F_1M_1M_2cdots M_n,F_2M_1M_2cdots M_n,cdots,F_nM_1M_2cdots M_n,]\ &=[F_1(M)_1(M)_2cdots (M)_n,F_2(M)_1(M)_2cdots (M)_n,cdots,F_n(M)_1(M)_2cdots (M)_n]\ &=(lambda m.[F_1(m)_1(m)_2cdots (m)_n,F_2(m)_1(m)_2cdots (m)_n,cdots,F_n(m)_1(m)_2cdots (m)_n])M end{align}$

$egin{array}{r} ag*{$Box$} end{array}$

不動點在 $lambda-calculus$ 中佔有極其重要的地位，使用不動點組合子可以實現匿名遞歸操作，循環可以設計成函數的遞歸，從而 $lambda-calculus$ 有了足夠的能力表現出編程語言的分支和循環。使得在普通的編程使用中，能夠更廣泛地使用函數式編程。

下一節的介紹將會是 $lambda-$ 表達式的在一些具體的編程語言中的應用介紹，具體的暫時先介紹在python，c++，matlab中的語法和使用，期望能從三種簡單的示例學習中達到舉一反三的目的，從而進行更高效的編碼。