樹莓派、樹莓派之學習、樹莓派之教育

λ 運算︰概念導引《二》

150px-Greek_lc_lamda_thin.svg

λ 何謂也？

λ 表達式的『核心』理念是︰將『函數』應用於其『引數』；藉『抽象』形成『函數』。用著『簡潔』的『語法』，專注於『表徵』函數；視『函數』為計算的『規則』，深得『計算』之『內蘊』。其『語詞』表達『疏落』大方，概念『表現力』與『柔軔性』十足。故為『邏輯』、『數學』和『程式』理念之『聚寶盆』！！

辨明『異同』與分解『差別』是學習的功夫︰

真積力，久則入。

讓我們再次『觀止』λ 表達式的『定義』︰

變元集合 V = \{ v_1, v_2, v_3, \dots, v_n, \dots \}
抽象符號 『 λ  』與『 . 』，符號本身不是λ 表達項
結構括號 『 ( 』與『 ) 』，括號本身不是λ 表達項

λ 表達式的論域集合 \Lambda，由下面三條語法歸納定義︰

一、如果 x \in V ，那麼 x \in \Lambda

二、如果 x \in V 而且 M \in \Lambda ，那麼 ( \lambda x. M ) \in \Lambda

三、如果 M, N \in \Lambda ，那麼 ( M \ N) \in \Lambda

假使觀察一個合乎語法的 λ 表達式 (\lambda f. (\lambda x. (f x)))，然後問著『 f 』變元是指『什麼』？這個表達式最內層的 (f x) 是函式的應用，明寫 f 是某個函式，然而如何計算卻隻字未提。如此看來，所謂的『變元』也可以是『函式』。那要怎麼『詮釋』那個『 λ表達式』呢？由於我們不知道 f, x 指的是什麼？也可以說它們『未被定義』，假使『給與定義』，我們或許可以講『在這個解釋下』，該個『 λ表達式』的『語意』是『□□□』。比方談著『用量角器量角度』一事，假使︰

f =_{df} 用量角器量角度
x =_{df} 東西的角度

，那麼 (\lambda f. (\lambda x. (f x))) 是說︰拿某種『待指定』的量角器來量『尚未說』之物的角度。

要是講到『計算某種三角函數的數值』時，設想︰

f =_{df} 某種三角函數的計算
x =_{df} 角度

，那麼 (\lambda f. (\lambda x. (f x))) 是說︰用某個『待指定』的三角函數來計算『未輸入』的角度。
……

由於每個『變元』的『論域』未被定義，所以各種『詮釋』都是『可能的』，因此說『函式建構』是『抽象』的，『應用化約』是廣義的『計算結構』之『同等性』。這也使得『應用化約』成為『 λ 運算』的『核心原則』，也就是說『 \beta 化約』是最重要的『轉換規則』。

如果從『輸入 Input \Rightarrow 處理 Process \Rightarrow 輸出 Output』的 IPO 觀點來看『計算系統』，『 λ 運算』是一個以『計算規則』為『中心』的『演算法』之語法。利用『應用化約』將『輸入變元』盡可能的化約成為也許『存在』之『最簡表達式』，而這個『最簡表達式』就是此『 λ 運算』的最終『輸出結果』。用著『不同』的『計算方法』或者說『計算結構』是可以得到『相同』的『計算結果』也許講『最簡結構』。然而『應用化約』卻有可能遭遇到變元的『命名衝突』之問題，就讓我們看看這個問題的原因以及將要如何去解決的吧。

考慮三個 λ 表達式 x、(\lambda x. M) 和 ((\lambda x. M) x)，我們要如何看待這些『 x 變元』呢？對於第一個式子 x，人們說它是『自由的』Free，因為它與其它表達式都無關，變元 x 就是指它自己。對於第二個式子 (\lambda x. M)，由於變元 x 是『運算規則』M 的『輸入變元』，人們說它是『受約束的』Bound。況且它還是『虛名』的，假使將『運算規則』如果想像成一個『黑箱系統』，那麼內部『運算方法』早已經是『設定好』的『圖靈機』── 比方輸入處系統內叫做 M_i ──，如此那個變元 x 就是 x =_{df} M_i 了，也就是說『被束縛』了。對於第三個式子 ((\lambda x. M) x) 來講，第一個 x 變元的出現是受約束的，然而第二個 x 變元的出現卻又是自由的，所以可能引發『混淆』，於是在『應用化約』時也許會產生『錯誤』或『歧異』。因此就必須要『辨明』一個 λ 表達式中的每一個變元『自由與否』的屬性。這兩個性質可以如下歸納的定義︰

假使 FV, BV 表示『自由變元』與『受約束變元』的『語法函數』syntactic functions︰

FV(x) =_{df} 的值是『自由變元』的集合，
BV(x) =_{df} 的值是『受約束變元』的集合。
x 是所指 λ 表達式的任意變元
M, N 是所指  λ 表達式的任意構成項── 該式在建構過程中的各個合乎語法的 λ 表達式 ──。

\forall x, \ FV(x) = \{ x \}
\forall M, N \ FV((M \ N)) = FV(M) \cup FV(N)
\forall x, \forall M, \ FV((\lambda x. M)) = FV(M) \setminus \{ x \}

\forall x, \ BV(x) = \Phi
\forall M, N \ BV((M \ N)) = BV(M) \cup BV(N)
\forall x, \forall M, \ BV((\lambda x. M)) = BV(M) \cup \{ x \}

通常『直覺知道』是一件事﹐『清晰定義』卻是另一件事，有時越是『精確』定義越難『把握』重點，『取捨之道』總落在『清楚思考』。

假使說有一個 λ 表達式 M 沒有自由變元，也就是說 FV(M) = \Phi，這時 M 稱作一種『組合子』combinator ── 它與『組合邏輯』Combinatory logic 有關 ──。如果從計算機器 的角度來看，組合子是『自足的』，它已經『完整封裝』不再需要任何其他輸入。某些組合子在『 λ 運算』的發展歷史上有著顯著的地位，簡短的講它們深化了人們對一些『基本概念』的『理解』。舉個例說，你會怎麼『詮釋』下面這兩個 T, F 組合子的呢？

T =_{df} (\lambda x. ( \lambda y. x))

F =_{df} (\lambda x. ( \lambda y. y))

既然已經知道了『命名』的變元之『自由』、『約束』和『此自由彼約束』性質，就可以談及在某一個『 λ 表達式』中，該式所構成的『表達項』如何『替換』Substitution 的作法，此處 A[x := M] 是指︰

將 A 『表達式』中所有『自由出現』的『 x 變元』，都使用 M 『表達項』來取代。

我們可以歸納的定義如下！

x, y 是所指 λ 表達式的任意變元
A, B. M, 是所指  λ 表達式的任意構成項── 該式在建構過程中的各個合乎語法的 λ 表達式 ──。

一、 x[x := M] \equiv M

二、 y[x := M] \equiv y，只要 y 變元不是 x 變元

三、 (A B)[x := M] \equiv (A[x := M] B[x := M])

四、 (\lambda x. A) [x := M] \equiv (\lambda x. A)

五、 (\lambda y. A) [x := M] \equiv (\lambda y. A[x := M] )，只要 y 變元不是 x 變元

『第一條替換規則』就是說我們要將 M 取代 x 變元之此同一件事。『第二條替換規則』是講 y 變元和 x 變元無關，無法談替換的事情。『第三條替換規則』說︰對於『應用化約』來講，替換是『分配』於『前後』表達項的。『第四條替換規則』類似『第二條替換規則』，因為『抽象函式』之變元『名字』是『虛名』的，所以該替換沒有作用。『第五條替換規則』就像『第一條替換規則』裡所說的一樣。 至於說『定義符號』 =_{df} 並不在『  λ 表達式』的構成裡，它是一種『縮寫』，目的是為了『清晰易讀』屬於表達『約定』的『改寫方法』，基本上與『替換』根本無關。

 

─── 待續…… ───