作者iamstudent (stu)
看板C_and_CPP
標題Re: [問題] 請問有哪種程式語言能做到數學的自動證明
時間Tue Mar 27 15:39:58 2012
以前在大學部的時候
學過計算理論
目前還隱約記得
有許多問題本身就是non determinable
而且大多問題
都是不可能以程式解答的
如果可以，則能導出矛盾
Halting problem：
不可能寫出一個程式
它能判斷任何程式是否永遠無法停止
證明應該很容易找到
基於這一點
以列舉方式來確認一個數學猜想
不可能以該程式能否停止來決定是否正確
因為無法決定該程式能否停止
這樣還不能夠證明
不可能以程式驗證一個數學猜想
另外一個比較有直接關係的
是Rice's theorm:
只要是non trivial的問題
就不可能寫出能判斷該問題的程式
這點與c, c++，或是不同的程式語言都沒有關係
純粹是邏輯上可以造成矛盾而不可能存在
當時我們老師舉了一個例子
不可能寫出一個c程式
能夠正確檢查所有c程式碼在執行之後
是否會印出Hello World
即使是這麼簡單的問題
也是non trivial的
--
※ 發信站: 批踢踢實業坊(ptt.cc)
◆ From: 140.113.210.62
→ damody:你們老師的例子舉的不好的感覺 03/27 19:58
→ iamstudent:剛剛看了上面的討論串，我想我可能誤解原問想要的東西 03/27 20:25
→ iamstudent:不過那個"不好的"例子確實可以證明不可能 03/27 20:27
→ iamstudent:證明的方法我有找到，只是我已經看不太懂了 XD 03/27 20:28
→ MOONRAKER:他老師舉的例子沒錯，這就是停止問題的敘述。 03/27 21:45
→ MOONRAKER:比較generic的講法是︰不可能存在程式 s 檢查任意兩個程 03/27 21:46
→ MOONRAKER:式 p, q 後，斷定兩個程式會輸出相同的結果 03/27 21:46
→ MOONRAKER:注意那個「任意」，就是它使得這種事情不可能 03/27 21:47
→ MOONRAKER:不過你的確誤解了，機械證明跟停止問題是兩回事 03/27 21:47
→ MOONRAKER:自有計算以來就有停止問題，但是機械證明也一樣有人在用 03/27 21:48
→ MOONRAKER:歷史至少30年 03/27 21:48