若曾經接觸過停機問題（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演算這類探討運算的模型，對今日的開發者依舊重要的原因。在電腦發明之前，它們就在探討更根本性的（數學）運算問題，而試著以這類運算模型探討問題，才能在探討的過程中，順道俯拾有益於未來解題時的各種思考。