【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做为补充: