1. 三条定律：交换律、结合律、吸收律（对于半格是幂等律），吸收律包含了幂等律

2. 上下界：交半格每对元素都有唯一最大下界，并半格每对元素都有唯一最小上界，格每对元素都有唯一最大下界和唯一最小上界

3. 格定义一个偏序，偏序有三个性质：自反性、反对称性、传递性

4. 格与偏序的关系：每个格对应一个偏序，但不是所有偏序都对应一个格，要满足每对元素都有唯一最小上界和（或，对于半格）唯一最大下界。如果集合中的任何一个子集（包括空集）均存在最小上界和最大下界，那么对应一个完备格

5. 任何元素有限的格都是完备格，格中的交运算和并运算对于其定义的偏序来说是单调的

6. 格的乘积、和、提升、映射仍然是格，利用这个性质，可以在已有格的基础上增量地构造描述能力更丰富的格，这种技术称为论域精化，是提高程序静态分析精度的重要指导思想之一

春秋十二月 2023-09-06 23:39 发表评论