Computable Functions are Monotonic

往 Nottingham 的公車上，我問 scm 老師 Intro. to FP 9.2.2 節的一個敘述：computable functions 必定是 monotonic。這裡採用的 ordering 在書上稱為 approximation ordering，是一種 (complete) partial ordering。以 Peano (natural) numbers 為例，Peano numbers 要嘛是零（zero），要嘛是某個自然數的後繼者（suc n）。在計算的世界裡，每個型別下都還有一個值 bottom（就是 _|_ 這個符號），代表「算不出來」。Approximation ordering x <= y 的意思是 x 是 y 的一個「近似值」。對於 Peano numbers，approximation ordering <= 可以這麼定義：

• bottom <= n for all n;
• zero <= zero;
• suc m <= suc n if m <= n.

（Hope it's reflexive, transitive, and anti-symmetric.）所以 bottom 是這個 ordering 之下的最小元素，suc (suc bottom) <= suc (suc (suc (suc zero))) = 4，但 3 和 4 之間沒有次序。Monotonicity of computable functions 說，當 f 是個可計算的自然數函數，我們就有

x <= y implies f x <= f y

直覺地講，approximation ordering 衡量的是我們能掌握的資訊量。Monotonicity 告訴我們，輸入的資訊愈多，輸出的資訊就愈多。

怎麼證明這件事情呢？我想到曾經在 Planet Haskell 上面看到一篇文章〈How many functions are there from () to ()?〉，談的正是類似的主題，不過裡面只處理了最簡單的 unit type。Peano numbers 似乎難一點。首先不妨假設 x = bottom，因為倘若 x <= y，我們一定可以不斷把兩邊最外側的 suc 拆掉，讓左邊露出 bottom。（x = zero 的情況是簡單的。）假設找得到 y 使得 f x > f y，我們想導出矛盾。

接下來是在車上的想法，但我在旅館裡面要把它寫下來的時候發現錯了。我試圖證明，因為 f bottom = non-bottom（f x > f y >= bottom），f 必為常函數，否則 Turing-recognizable & co-Turing-recognizable implies decidable，用 f 就能讓 halting problem 變為 decidable。如果 f 的確是常函數，f x 就不可能嚴格地大於 f y，得到矛盾。可惜證明「f 是常函數」那一步是錯的，f 並沒有使 halting problem 變成 co-Turing-recognizable。現在我暫時想不到比上面引用的那篇文章更好的方法證明整件事情，而那篇文章主要是在 Haskell 底下談的。

--
我還是先多寫一點中文吧，讓附近的人比較容易看…