找出該證的性質，然後證明它

研究所入學那天，老師照例勉勵新生們。多年後，除了指導老師說的一些事，我只記得這麼一段話：「所謂做研究，就是找個好問題，然後解決它。前者通常比後者難。」

很遺憾，剛到所上誰都不認識的我竟不記得是誰下了這麼一個雋永深刻的評語。

過去兩週試著證明一個演算法的正確性，本希望能在一週內解決，硬是拖了一倍的時間。這時回想起那句話，倒是在小尺度內有了類似的感觸：做我們這種研究，就是找出那個該證的性質，然後證明它。前者通常比後者難。

所謂一個演算法「正確」，指的是其算出的東西符合規格。這當然是我們最後希望證明的性質。但通常這無法直接證。我們得證明該演算法滿足某些不變量 (invariant). 理想上，不變量在設計演算法時就該推導出來。實際上，我們常得要證明別人的演算法，而對方對不變量只有一個籠統模糊的描述；或著我們討論的是還在成形中的演算法。這時只好猜。

於是我們靠感覺和經驗猜：整個演算法如果有效，某個性質要應該成立吧。理想情況是立刻用一個歸納證明漂亮搞定。實際上，一個大定理通常無法整塊一口氣證出來，得拆成幾個輔助定理。怎麼拆呢？照經驗，並靠著對問題的了解。嗯，也許它會對，是因為這個、這個、和那個。拆成三個小性質，把最明顯、應該不會不成立的擱一旁，從問題較大的開始證。

那麼，開始歸納證明囉？硬推幾步後常會發現這樣行不通。為了歸納證明，我們得證一個更廣泛、更強的性質。廣泛化的方法很多種，要挑哪個？只好再靠經驗猜了。這是一個不斷調整的過程：你證的性質得強到可提供足夠的歸納假設，又不至於過強到證不出來。總之，分出幾個 case，推了幾步之後，開始三心二意了。這樣對嗎？

往往事情就是愛捉弄人。好不容易證完第一個補助定理、第二個補助定理，再回頭看當初擱一邊的、覺得很明顯應該會對的那個補助定理，其實是錯的。

啊，只好再重新開始了。追根究底，那是因為我們還不夠了解手上的問題。要正確地把性質切成小塊，我們得對問題有全盤的了解。但全盤的了解又根基於從每個細節的運作中學到的經驗。而人腦能同時處理的問題複雜度有限，於是只好反覆東想、西想，不知該由上往下、還是由下往上？

用 Coq, Agda 之類的證明輔助程式可能讓情況更糟糕。我原以為電腦適合證明有很多 case 的性質，因此把定理放到 Coq 或 Agda 裡，希望靠著問答和填空格就可以糊裡糊塗地把性質證出來。結果我得到的慘痛教訓是：若不先想清楚，證明輔助程式剛好賦予你在錯誤的路上走得更遠的能力。我寫了幾百行的證明，迷失在許多細節裡，才發現此路不通。也許證明還是得先在紙上做一遍吧？

等到終於找到那組對的性質，也終於確定把這問題搞懂了。證明可能不過是十幾分鐘的事情。「就這樣？」這很明顯嘛。怎麼沒早點想通呢？

這就是做我們這行研究呀。