• 一、概念
• 二、什麼是反證法
• 三、證明停機問題無解
  • 1. 假設能寫出停機函式check_halt(program, params)
  • 2. 定義一個呼叫了check_halt的會觸發死迴圈的函式self_root
  • 3. self_root(self_root)觸發矛盾

一、概念

能不能寫出一個程式check_halt，傳入程式program和引數params，返回這個程式是否會結束？

比如，求和函式sum計算[1,2]，check_halt(sum, [1, 2])應該返回true

雖然我們特別想要這樣的功能，讓我們提前做災備工作，避免重大的程式風險，但是這是一個不可解的問題，可以用反證法來證明。

二、什麼是反證法

就是先假設“命題的否定形式”成立，再根據假設推匯出矛盾的結果駁倒假設。

舉例：
證明“不存在最大的正整數”。

這個問題其實問出來，一般人會覺得你無聊吃飽了撐著，只會傻不拉幾的說：“不TM不是常識嗎？這還用證明？”（No，科學是要證明的！）

我們用反證法證明一下：

1. 假設“存在最大的正整數”，這個數為M
2. 那麼M+1比M大，這與假設矛盾

所以，“不存在最大的正整數”

三、證明停機問題無解

1. 假設能寫出停機函式check_halt(program, params)

如果能停止，返回True；如果不能停止，返回false

以下是虛擬碼

def check_halt(program, params):
    return True Or False
 

2. 定義一個呼叫了check_halt的會觸發死迴圈的函式self_root

如果check_halt(program, program)返回true，就進入死迴圈；
如果check_halt(program, program)返回false，就返回0

def self_root(program):
    if check_halt(program, program):
        while True:
            # 如果停機就進入死迴圈
            pass
    else:
        return 0

注意：check_halt的兩個引數都是program

3. self_root(self_root)觸發矛盾

1. 假設self_root(self_root)會結束執行
   那麼check_halt(self_root, self_root)返回true，self_root會進入死迴圈，不會結束，與假設矛盾
2. 假設self_root(self_root)不會結束執行
   那麼check_halt(self_root, self_root)返回false，self會結束，又與假設矛盾

綜上所述，check_halt不能寫出，所以停機問題是無解的