如何理解萊斯定理對程序靜態分析的限制？

01-28

一般對於靜態分析的限制都推導為停機問題或用萊斯定理解釋，有一點不太清楚的是，我的理解是根據上述的限制導致是不能找出針對某個語言的某種非平凡屬性通用的判斷方法，但是在一些情況還是能夠完美解決的（也不是近似解），那麼有沒有方法能夠準確描述出在哪些條件下能夠判斷哪些不行，舉個例子就是有沒有理論可以計算出對於數組越界的判定程序可以判定出哪些程序有數組越界的問題，哪些程序是它判斷不了的？另外是不是可以理解為因為邏輯悖論的存在才使得這種通用判斷方法等不可判定問題的存在？
稍微補充一下：本質上說是哥德爾不完備定理的作用導致沒有通用的判定方法，那麼它具體是怎麼限定或如何作用的，畢竟感覺停機問題的證明也只是得出一個結論而沒有說明具體的原因（只是通過反證法歸謬，而沒有說明產生此種現象背後的因素是什麼）。即在某個問題中能不能有一種方法可以找到其中導致不可判定的因素，或者去尋找這種因素的思路。那麼在具體的靜態分析處理實踐中是如何考慮這些問題的影響呢？在設計一種靜態分析演算法的時候如何去全面和正確評估此演算法的計算能力，即它的sound和complete的程度？

數組越界問題沒仔細研究過，但是pointer analysis有很多這樣的結果。一圖勝千言：

這張圖是從底部那個POPL paper抄的，你可以詳細了解下。這篇文章有一些更general的關於data flow analysis的複雜度結論，可以讀讀：On the complexity of flow-sensitive dataflow analyses

被邀請了三次，還是回答一下吧。首先，題主的要求太強了，如果給定任意程序分析問題，我們都想要知道這個問題是不是可判定的，那麼這就和回答「任意問題的可判定性」一樣，根據哥德爾不完備定理必然是沒有演算法可以求解的。

但是，我們可以把題主的目標弱化一些。即：在萊斯定理的空間之外是否還存在可判定的問題？那這個答案就是肯定的了。要理解這個問題，我們首先要理解萊斯定理定義了哪些東西。下面是維基百科上的定義：

Let S be a set of languages that is nontrivial, meaning

there exists a Turing machine that recognizes a language in S
there exists a Turing machine that recognizes a language not in S

Then, it is undecidable to determine whether the language recognized by an arbitrary Turing machine lies in S.

這個定義本身比較抽象。簡單來看，我們也可以認為S是程序的一個屬性。如果這個屬性不對所有程序都為真或者為假，即非平凡，那麼我們就不存在一個演算法來判斷某個程序是否具有這個屬性。這也是我在我的《軟體分析技術》課中採用的定義。

但是需要注意的是這裡的「程序」是用圖靈機編寫的程序。也就是說，如果我們限定到一個非圖靈機編寫的程序上，萊斯定理就不適用了。比如下面這個性質：

「給定無循環和函數調用的程序，判斷程序是否在某些輸入上會拋出異常」

「拋出異常」這個性質顯然是一個非平凡性質，但這個問題本身是可判定的，因為程序實際限定到了一個比圖靈機表達能力更弱的子集上面。

另外，我們也可以把問題改成：在知道的時候返回程序是否具有屬性S，在不知道的時候返回不知道，原問題也就可以判定了。

所以，我們可以從幾個方向來擺脫萊斯定理的限制。一方面，我們可以設計一些非圖靈完整的編程語言，這些編程語言的某些性質是可以判定的，同時編程語言本身在一些領域也會非常有用。這類「領域特定編程語言」是編程語言設計研究的一個重點。另一方面，我們允許回答「不知道」，問題也就變得可以判定了。這就是程序分析研究的主要內容。

當然，我覺得題主問的可能是更終極一些的問題。即，給定一組想要判定的屬性，是否可以求出一個編程語言，對於該編程語言的任意程序均可判定這組屬性，且表達能力比它強的都不能判定所有屬性。這個問題本身應該是不可判定的，不過針對這個問題給出部分解法，或者針對這個問題的某些特化實例（比如屬性=不會停機）求解是理論界多年來的研究內容，不過目前並沒有產生類似萊斯定理這樣的普適性成果。

這個問題說明題主沒有清楚理解萊斯定理和判定過程。萊斯定理本質上說的是，對任意（程序的）非平凡指標集，停機問題或者歸約到這個指標集，或者歸約到這個指標集的補集。指標集直觀上描述的是程序的相同行為，一個集合 $A subseteq mathbb{N}$ 是一個指標集，如果 $A$ 滿足 $forall x,yin mathbb{N} [x in A wedge Phi_x=Phi_y ightarrow yin A]$ 。

如果題主例子中的所有存在數組越界問題的程序構成一個指標集，那麼根據萊斯定理，這個問題是不可判定的。如果不構成指標集，那麼萊斯定理就不適用。（當然，萊斯定理不適用並不代表該問題是可判定的。）特別地，直觀上存在數組越界問題的程序不構成一個指標集。

其次，這句話非常難以理解：

有沒有理論可以計算出對於數組越界的判定程序可以判定出哪些程序有數組越界的問題，哪些程序是它判斷不了的？

幫助題主澄清一下概念，如果一個程序是一個判定過程，那麼就不存在

哪些程序是它判斷不了的？

這種問題。

最後，關於題主想知道哥德爾不完備定理以及停機問題的所謂「背後的因素」，建議題主靜心學兩年數理邏輯和數學哲學。我所見過的幾乎任何試圖三言兩語講清楚其「背後的因素」的回答，對於初學者而言都是極具誤導性的。

所有關於程序行為的問題都是不可判定的。這已經是不爭的事實。例如，數組越界問題可能依賴於指針分析還有其他行為，而指針分析肯定是不可判定的。但是可以在一定假設下，對某類問題的求解可以確定的。例如，程序中沒有指針，類型嚴格等等。在實際工程中，不同領域軟體對語言的使用也是一個子集，這時候往往可以選擇比較適合的假設。

個人認為，從解決實際問題的角度沒有必要苛求100%的程序正確性驗證。