從萊斯定理出發看程式分析中的sound與complete
萊斯定理是計算理論中非常重要的結論，從它出發也可以明瞭的分析出針對圖靈完備語言進行靜態分析的理論上限。萊斯定理的定義是這樣的：
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.
定義首先說明了“非平凡性”這一概念，非平凡性指的是：如果一個屬性不對所有的程式都為真或假，即為非平凡。比如程式是否不存在陣列越界，是否不存在空指標解引用，都是對於程式的非平凡屬性。萊斯定理的內容即為：一個程式是否具備某種非平凡屬性這個問題如同停機問題一樣，是不可判定的，即不存在一個程式可以判定任意程式具有某種非平凡屬性。
既然有這種結論，是不是說明我們沒法做程式分析了呢？並不是，因為萊斯定理中的“程式”指的是用圖靈機編寫的程式。也就是說，如果我們限定到一個非圖靈完備語言編寫的程式上，萊斯定理就不適用了。比如我們限定程式不能使用迴圈，這時候一些非平凡屬性可能就是可判定的。這個時候我們所判定的程式集合是在一個非圖靈完備的DSL框架中。既然存在可判定的DSL，那麼對於圖靈完備語言所編寫的一部分程式也有可能是可判定的——也就是說，對於圖靈完備語言，一些情況下我們能做出正確的分析，一些情況下是無法判定的。
因此，我們需要規避一些不可判定的情況，對程式得出一個儘可能“正確”的分析。也就是說，我們的程式分析結果其實都並不是那麼“精確”——程式分析允許一定的不精確性。但是它們都是在“安全”或者說“保守”的方向上不精確。在不同的分析應用中，所謂“保守”的方向也各不相同。如通過到達定值分析解決下面這個問題：
這個問題中，在不知道定值是否會到達某點的情況下假設針對每個賦值變數都產生一個新的定值是保守的。如果得出的解認為不產生新的定值，那麼會將x視為迴圈不變數提出，這個錯誤的優化改變x的值。在可用表示式分析中，“安全”的定義就和到達定值不同。如果可用表示式沒有到達某個程式點，而得出的解表明到達了，則這是不安全的。因為如果一個表示式被認為是可用的，我們有可能會做一些比較危險的事情，例如刪除重複計算該表示式的指令。因此在設計一個數據流模式的時候，我們必須知道這些資訊將如何被使用，並保證我們做出的任何估算都是在“保守”或者說“安全”的方向上。每個模式和應用都要單獨考慮。
依據這個原則，我們的解要在“保守”的大原則下儘量做到精確。比如資料流分析大多采用迭代分析的框架，那麼解就要在迭代的過程中盡力向精確的方向靠近。使用術語來說明這個概念，sound static analysis就對應我們所謂的“保守解”，它是一種“過逼近”，能夠覆蓋完所有違反所要檢驗的屬性的場景，不過因為它考慮程式中可能實際並不可行的路徑，所以會產生誤報。complete static analysis則與之相反，是一種“欠逼近”，它產生的解超過精確解，這些值保證都違反了所要檢驗的屬性，但是並不能覆蓋完所有的值，有漏報。考慮萊斯定理的概念，complete分析就是一種針對可判定情形的檢驗，對於其它情形則允許“不知道”，而sound分析則需要進行過度考慮，在許多情形下，靜態分析工具並不能做到sound，因為它需要探索過多的執行路徑，嚴重影響接下來分析的精確度，以至於無法得到有效的結果。