若曾經接觸過停機問題(halting problem)的開發者,應該都理解一件事,「程式無所不能」是錯的!但是,從實務面來看,開發者為什麼要知道這件事?

停機並不是唯一無解的問題,證明問題無解可以避免未來徒勞無功,然而,這件事的背後,或許還有更重要的目的存在。

Y Combinator存在x函式?

至今的專欄已經談過多次lambda演算了,具備一級函式的語言,多半也會強調其基於lambda演算的重要性,然而究竟是為了什麼?探討遞迴這在lambda演算中是怎麼一回事,可以得到一點靈感。

lambda演算從頭至尾都使用匿名函式,就算是遞迴函式,也必須是匿名函式,例如,階乘函式必須是fact => n => n < 2 ? 1 : n * fact(n - 1)形式,然而怎麼執行它?fact從何而來?如果有個函式y,可以產生fact傳給階乘函式,就可以執行階乘運算了。

可以達到此效果的y函式是存在,也可以導證出來的。第一步通常假設y內部有個x函式,呼叫之後,就可以產生fact需要的遞迴函式,若以JavaScript為例,y會是f => (x => f(n => x(x)(n)))(x => f(n => x(x)(n))),然後,就可以開心地進行遞廻了,探討Y Combinator的文件中,而故事往往到這邊,就結束了……

等一下!你真的仔細想過,為什麼Y Combinator長成這樣嗎?你找到x了?

更進一步看看吧!如果只給y一個f,會得到部份套用函式(x => f(n => x(x)(n)))(x => f(n => x(x)(n))),將後方的x => f(n => x(x)(n))作為前方x的值套用後,此時,我們會得到f(n => (x => f(n => x(x)(n)))((x => f(n => x(x)(n))))(n)),也就是傳入f的是n => (x => f(n => x(x)(n)))((x => f(n => x(x)(n))))(n),而我們就叫它是fact好了。

繼續用個n來套用fact,就會發現開始重複前一段的過程,最後傳入f又會是fact,也就是f(fact)套用n執行過後又會是fact,呼叫再多次都一樣,你找到了f的不動點(Fixed-point)。

而說明不動點的更簡單例子是,若有個函式f(x),有個值v令f(v) 結果仍為v,v就是f(x)的不動點,例如,0和1是函式f(x) = square(x)的不動點,因為f(0)為0,f(1)為1。

Y Combinator實際上為f產生的是不動點,以不動點執行f,可以得到x函式,進一步以x產生真正的遞迴函式嗎?結果還是得到不動點。

如果想打破砂鍋問到底,若以人力來進行運算,算到死都不會知道x從何而來,如果是透過現代的電腦來計算,就是看什麼時候堆疊錯誤發生了,此時,你覺得x真的存在嗎?

判定匿名函式等價?

在先前專欄〈ES6與lambda演算〉中談過,如何使用匿名函式為數字編碼,現在進一步地想一下,如果有個代表數字的匿名函式,可以判定它與另一個代表數字的匿名函式相同嗎?也就是現在打算判斷數字的相等性,這需求可否實現?

如果限定在判定數字編碼的相等性,這需求是可以實現的!

不少程式語言中都有個特別的值,代表著什麼都沒有,名稱會是nil、null或undefined之類,通常也可以與任何值比較相等性。如果在JavaScript實現lambda演算,可能也會萌生為undefined編碼的念頭,然而,馬上就會遇到一個問題,像是v === undefined這樣的需求,我們該如何使用lambda演算來解決?

也許有人會說,上頭不就寫出是===了嗎?不行!===是JavaScript的東西,想要的會是個通用的eq(f1)(f2),可以判定匿名函式f1、f2是否等價,而且對於JavaScript中的===對函式來說,比較的其實是函式物件的記憶體位址,而不是比較匿名函式是否等價,因此單純像是(x => x) === (x => x)的結果會是false,實際上,就lambda演算來說,兩者是等價的。

試著呼叫匿名函式,看看它們是不是傳回相同的值呢?因為是eq、必須是通用的,因此沒辦法預期會傳入什麼匿名函式,也就無法確定呼叫匿名函式時該傳入什麼引數,而且別忘了,值全部都使用匿名函式編碼了,傳回值也會是匿名函式。於是,問題回到原點,如何確認傳回的兩個匿名函式等價?

也許可以像Y Combinator那樣,先假設eq是存在的,再逐步導證,或許最後同樣可以拖泥帶水,不用正面回答eq是什麼?可惜的是,若eq(f1)(f2)會是true,試著基於eq存在而進一步建立起的其他函式,卻會要求eq(f1)(f2)必須是false,反之亦然,形成矛盾,使得這樣的eq不存在!

決策問題

能夠判定程式是否停機的halt函式,以及能夠判定任意兩個匿名函式是否等價的eq函式,這些都是屬於決策問題(Decision problem),也就是面對的問題,答案上都只需要給出是或否,對於這類問題,若存在演算法,保證可以在有限時間內回答是或否,稱之為可決策的(decidable)或可運算的(computable)問題。

判定是否停機與匿名函式是否等價的函式,一開始都假設其存在,最終發生給出的答案自相矛盾,就如同「絕對不說真話的騙子告訴你:『我現在正在說謊!』」本身就是悖論。別想以邏輯判定騙子說的那句話是真或假,自相矛盾的東西也寫不出演算法,因此,停機或等價函式是不可運算的問題。

回到Y Combinator,你覺得x是否存在?這也是個決策問題,然而,Y Combinator產生不動點,試圖一直執行只會永遠不會停止,無法在有限時間內知道x到底存在或者不存在,Y Combinator的x是否存在,這個問題無從回答。

存在著不可運算的決策問題,這事實對熱愛程式設計的人是個打擊(對熱愛數學的人也是),這表示程式並非無所不能,只是這又怎麼了嗎?在知道這事實之前,許多開發者還不是照樣在寫程式。

從戲謔的角度來看,這件事很重要,就像程式設計界常看到類似的說法「我不知道這為什麼行不通!」以及另一個「更可怕的事情是,我不知道這為什麼行得通!」

從務實的角度來看,山不轉路轉!Y Combinator就是個例子,既然算到死,它都不會交代x從何而來,那就別打破砂鍋問到底了,適可而止。給個邊界,適當時機不再執行傳入f的函式,就可以停止下個不動點的產生,這就是遞迴的停止條件設定了。

在「山不轉路轉」之前

能夠證明決策問題不可運算,本身就是個成就了,這表示未來不用再為這問題徒勞無功,然而,在山不轉路轉之前,如何能知道這方式行不通,或許才更為重要。無論最後的事實是可運算或不可運算,事實的結論之外,還有另一個重點,也就是,理解一件事是否可解決的過程。

正是因為有這樣的過程,才能在最後,就算證明了問題不可運算,也還是能從過程中找出夠用或者是近似的方法。例如捨棄通用性,不追求通用的eq函式,而針對特定資料撰寫特定的相等性判定函式;不尋找真正產生遞迴的函式,只需要有不動點,就可以達到想要的遞迴目的等。

這就是lambda演算這類探討運算的模型,對今日的開發者依舊重要的原因。在電腦發明之前,它們就在探討更根本性的(數學)運算問題,而試著以這類運算模型探討問題,才能在探討的過程中,順道俯拾有益於未來解題時的各種思考。

作者簡介


Advertisement

更多 iThome相關內容