【Static Program Analysis - Chapter 4】格理論(Lattice Theory)與程序分析

# 從一個例子提及，

**任務：給定這樣一段代碼，假設咱們想分析出這段代碼中，每一個數值型變量和表達式的符號，即正數，負數或0。**

此外，還有可能出現兩種狀況就是：

1.咱們沒法分析出結果，即咱們沒法肯定符號，用(?)表示；

2.有些表達式的值並非一個數字（例如，有多是個指針）或者在執行的過程當中沒有被賦值（有多是由於對於給定的輸入，沒有執行到，unreachable），用(⊥)表示。

所以，對於每個變量或者是表達式，咱們會有5種結果(這裏將其表徵成「格」的形式)：

(?)可能的緣由是：

1.執行屢次，變量c是正數或者是負數的結果都出現過。因此標記爲(?)更加保險；

2.分析方法沒法證實結果的肯定性。如，執行屢次變量都是正數，可是分析方法沒法證實變量必定是正數。

 # 格理論(Lattice Theory)

## 偏序集合(Partially ordered set，簡寫poset)

首先了解一個概念叫*偏序集合*，（英語：Partially ordered set，簡寫poset）是數學中，特別是序理論中，指配備了部分排序關係的集合。 這個理論將排序、順序或排列這個集合的元素的直覺概念抽象化。這種排序沒必要然須要是所有的，就是說沒必要要保證此集合內的全部對象的相互可比較性。部分排序集合定義了部分排拓撲。（更多詳細的介紹見維基百科）

理解偏序 & 全序:

偏序：集合內只有部分元素之間在這個關係下是能夠比較的。
好比：好比複數集中並非全部的數均可以比較大小，那麼「大小」就是複數集的一個偏序關係。 

全序：集合內任何一對元素在在這個關係下都是相互可比較的。
好比：有限長度的序列按字典序是全序的。最多見的是單詞在字典中是全序的。

 

偏序關係即給定集合S，「≤」是S上的二元關係，若「≤」知足：

1. 自反性：∀a∈S，有a≤a；
2. 反對稱性：∀a，b∈S，a≤b且b≤a，則a=b；
3. 傳遞性：∀a，b，c∈S，a≤b且b≤c，則a≤c；

則稱「≤」是S上的非嚴格偏序或自反偏序。

 

全序關係即集合X上的反對稱的、傳遞的和徹底的二元關係（通常稱其爲≤）。

若X知足全序關係，則下列陳述對於X中的全部a, b和c成立：

• 反對稱性：若a ≤ b且b ≤ a則a = b
• 傳遞性：若a ≤ b且b ≤ c則a ≤ c
• 徹底性：a ≤ b或b ≤ a

 

注意：徹底性(全序)自己也包括了自反性。
因此，全序關係必是偏序關係。

 

## 格，a lattice is a pair(S,⊑) 

在數學中，格是其非空有限子集都有一個上確界（叫並）和一個下确界（叫交）的偏序集合（poset）。格也能夠特徵化爲知足特定公理恆等式的代數結構。由於兩個定義是等價的，格理論從序理論和泛代數兩者提取內容。半格包括了格，依次包括海廷代數和布爾代數。這些"格樣式"的結構都容許序理論和抽象代數的描述。（更多詳細的介紹見維基百科）

 

序理論定義

 考慮任意一個偏序集合（L,≤），若是對集合L中的任意元素a,b，使得a,b在L中存在一個最大下界，和最小上界，則(L,≤)是一個格。

這裏對於取a,b的最大下界的操做用{\displaystyle a\wedge b}表示；

對於取a,b的最小上界操做用 {\displaystyle a\vee b}表示。

有界格有一個最大元素和一個最小元素，按慣例分別指示爲1和0（也叫作頂和底）。任何格均可以經過增長一個最大元素和最小元素而轉換成有界格。

 

使用容易的概括論證，你能夠演繹出任何格的全部非空有限子集的上確界（並）和下确界（交）的存在。一個很重要的格的種類是徹底格。一個格是徹底的，若是它的全部子集都有一個交和一個並，這對比於上述格的定義，這裏只要求全部非空有限子集的交和並的存在。

例子：

任何一個有限的偏序集合能夠表示成一張哈斯圖（Hasse diagram，每一個元素表明一個節點，順序關係是邊的傳遞閉包，由低到高），如，

 

以上都是格，如下都不是格：

其餘一些例子：

 

## 不動點(fixed-points)

這裏引用王千祥老師的slide做爲補充: