程式等價的不可判定性（undecidability of program equivalence）

假設你重構了一個函數，想要一個工具來證明新版本在每個可能的輸入上都與舊版本行為相同。又或者你想檢查一個快速的最佳化常式與緩慢的參考實作計算的東西完全一樣。程式等價就是這個問題：「這兩台機器識別同一個語言（計算同一個輸入—輸出行為）嗎？」壞消息是：這不可判定。沒有演算法能對所有程式對判定它們是否行為等價。

形式語言是 EQ_TM =（(M1, M2)：M1 與 M2 識別同一語言），一個快速歸約就證明它不可判定。假設你有一個等價判定器。取任意機器 M 與任意輸入 w。造一台 M1，它忽略自己的輸入並模擬 M 在 w 上的執行，若 M 接受就接受；再造一台 M2，它單純拒絕一切（其語言為空）。那麼 M1 與 M2 等價，恰好當 M「不接受」w。所以等價判定器就能判定 co-A_TM，而後者連可識別都不是——矛盾。等價不可判定，事實上還不可識別。

這在真實工程裡咬得很重。沒有一個完全通用、永遠正確的方法能確認兩個程式可互換、確認編譯器最佳化保留了語意、或確認你的改寫沒有引入行為改變。一如既往，實務世界靠限縮問題來應付：對較簡單的模型（如確定型有限自動機）等價「是」可判定的，而對真實程式則靠測試、靠有界輸入上的等價檢查、或靠對每次編譯重新檢查的翻譯驗證來逼近。但那個通用的「這兩個任意程式一樣嗎？」按鈕不可能存在。