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 alln
;zero <= zero
;suc m <= suc n
ifm <= n
.
suc (suc bottom) <= suc (suc (suc (suc zero)))
= 4,但 3 和 4 之間沒有次序。Monotonicity of computable functions 說,當 f
是個可計算的自然數函數,我們就有x <= y
impliesf x <= f y
怎麼證明這件事情呢?我想到曾經在 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 底下談的。
--
我還是先多寫一點中文吧,讓附近的人比較容易看…
Labels: Computability Theory, CS
沒擔保說寫中文就有人看呀, ㄎ
至少少一個不看的理由 XD。
老闆人真好 〒△〒
Consider the following problem and a possible solution:
A preference relation is said to be weakly monotonic if and only if x y implies that y x. Show that if is transitive, locally nonsatiated and weakly monotonic then it is also monotonic
Solution
Suppose that x >> y.
Define = min {x1 – y1, …., xL – yL} > 0.
For every z in the consumption set, if z is less than distance of y, then x >> z.
By local nonsatiation there exists z* such that the distance from z* to y is < and y z*.
From the fact that x >> z* and weak monotonicity, z* x.
Part (iii) of Proposition 1.B.1in the Text is implied by transitivity.
Therefore y x and so is monotonic.
do you think this solution answers the Question ?
<< 回到主頁