Re: [問題] 無法判定程式終結

[xcycl (XOO)]

※ 引述《dharma (達)》之銘言：
: 演算法之道裡寫道：
: ...無法判定程式終結，這個結論對程式設計來說意義重大。就是這個緣故，程式永遠不
: 會是全自動的，即不可能由程式自己來寫程式、啟動程式、控制程式。也就是說，像「駭
: 客任務」那樣的情景永遠也不會出現。而隱含的意義是程式設計永遠也離不開程式設計師
: 。...
: 書上這個論點
: 是現在學術和產業界的共識嗎？
: 是不是只有人類開發出仿生腦
: 才會有真正的人工智慧
: thank
停機問題（halting problem）是計算理論中最基本的常識。

首先，理論上我們簡單將程式分類成

1. 若存在某個演算法，對給定的問題如果有解，
可以在有限時間內給出答案，稱為「可計算」 computable (或是 semi-decidable）
2. 另一方面，不只是有解的情況，若是沒有解也可以在有限時間內回答，
則稱為「可判定」 decidable。

而 halting problem 的問題是：給定任意程式 P ，斷定它是否會停止。
很明顯的這是可計算的問題，因為只要去執行 P ，
若 P 在有限時間內結束，可以 P 在有限時間內得到答案。
但這個解法並不能在有限時間內推斷 P 「不會」結束。
（這邊提到的程式並不包含有輸入的程式。）

以上這個解法不成功，那是否存在另一個程式可以做到呢？也不行。
很久以前就已經有數學證明，不存在這樣的程式或機器。
原文接下來的推論，我認為是過於粗糙簡略了，按下不表。

不過呢，halting problem 討論的是「所有可能的程式」，
但可以把問題縮小到一些比較簡單能夠判定程式，
有些程式語言甚至保證所有的程式都會終止，像是 Agda
或是理論上的語言 polymorphic lambda calculus。

--
※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 1.162.4.165
※ 文章網址: http://www.ptt.cc/bbs/Programming/M.1403603605.A.E4A.html
→ freef1y3:保證所有程式都會終止！好神奇
→ freef1y3:那我可以用Agda來計算3n+1數列嗎？
→ freef1y3:若可用Agda來計算3n+1數列，Agda又保證
→ freef1y3:所有程式都會終止，那是不是就證明了
→ freef1y3:3n+1數列一定會終止呢？
推 freef1y3:還是說Agda的表達能力無法計算3n+1數列呢
推 freef1y3:(3n+1數列指的是3n+1 Conjecture)
→ scwg:Agda 的終止判定會找不到「証據」可以保証一
→ scwg:定會終止, 於是回報 warning / error
→ scwg:在 Coq 裡寫程式的人要主動提供「線索」
→ scwg: (metric, 須非負且遞減), 3n+1 還沒有已知的
→ scwg:metric, 因此 Coq 也不會接受
推 freef1y3:原來如此，我就在想如果所有程式都能終止
→ freef1y3:那這個語言的表達能力一定很有限
→ Killercat:不可能 這其實也是zombie thread的問題
→ xcycl:其實可以寫 Turing complete 的語言
→ xcycl:只是一次只能做有限多步的運算而已
→ xcycl:實務上沒有太大的問題