【性质】
1. 判定两个完全格L和M能否构成伽罗瓦连接，即抽象化函数α: L—>M是否完全加性的，或具体化函数γ: M—>L是否完全乘性的
2. 构造抽象化函数和具体化函数，即对于一个Galois连接（L, α, γ, M），给定α可通过γ(m) = ⊔{l | α(l) ⊑ m}确定γ，这对于所有m成立，且由于α是确定的，因此γ是唯一确定的。取最小上界是为了保证m描述的L中元素对于所有安全地描述了M中α(l)的l是安全的；给定γ可通过 α(l) = ⊓ {m | l ⊑ γ(m) } 确定α，其唯一性和取最大下界的原因类似前面
3. 帮助定义分析具体格源值到抽象格属性的正确性关系与表示函数。设有Galois连接（L, α, γ, M），R: V×L —>{true, false}为正确性关系，由表示函数β:V—>L生成，定义S: V×M —>{true, false}，则有v S m ⇔ v R (γ(m)) ⇔ β(v ) ⊑ γ(m) ⇔ (α◦β)(v) ⊑ m，即S为正确性关系，由表示函数α◦β: V—>M生成
4. 抽象化上迭代多次具体化+抽象化，结果等于一次抽象化，即α◦γ◦α = α；具体化上迭代多次抽象化+具体化，结果等于一次具体化，即γ◦α◦ γ = γ。这个性质被用于基于约化算子构造的伽罗瓦插入（特殊的伽罗瓦连接：具体化为单射，抽象化为满射）的证明
【组合】
分三大类，即顺序组合、并行组合和函数空间。为简化描述，下文简称Galois为G
1. 顺序组合：取第一个G连接的具体格，最后一个G连接的抽象格，从第一个G连接到最后一个G连接组合各抽象化函数，从最后一个G连接到第一个G连接组合各具体化函数。例如，设（L₀, α₁, γ₁, L₁）和（L₁, α₂, γ₂, L₂）都是G连接，则（L₀, α₂◦α₁, γ₂◦γ₁, L₂）也是一个G连接
2. 并行组合：有六种方法，即独立特征、相关性、直积、直张量积、约化积、约化张量积，前两种用于组合分别针对不同结构多个分析的多个G连接为一个G连接。中间两种组合针对同一结构多个分析的多个G连接为一个G连接，后两种组合针对同一结构多个分析的多个G连接为一个G插入。独立特征、直积、约化积与其它方法的区别是两对抽象化函数与具体化函数之间没有相互作用，会损失分析结果精度，本质就是P(A)×P(B)和P(A×B)的差别（P为幂集，A、B为集合）；独立特征与直积、约化积的区别是具体化函数定义不同（抽象化函数相同），前者是两个具体化函数的二元组即γ(m₁, m₂)=(γ₁(m₁), γ₂(m₂))，后者则是最大下界即γ(m)=γ₁(m₁)∧γ₂(m₂)
3. 函数空间：分为总函数空间和单调函数空间。对于前者，设（L, α, γ, M）为一个G连接，S为一个集合，f为S到L的函数，g为S到M的函数，因L和M为完全格，故由f或g构成的函数集合为总函数空间，则得到一个G连接（S—>L, α', γ', S—>M），其中α'(f)=α◦f, γ'(g)=γ◦g。对于后者，设（L₁, α₁, γ₁, M₁）和（L₂, α₂, γ₂, M₂）为G连接，f为L₁到L₂的函数，g为M₁到M₂的函数，因每个L及M为完全格，故由f或g构成的函数集合为单调函数空间，则得到一个G连接（L₁—>L₂, α, γ, M₁—>M₂），其中α(f)=α₂ ◦f ◦γ₁，γ(g)=γ₂◦ g◦ α₁
【应用】
当要做数据流分析的一个完全格L不满足升链条件时，除了直接对L运用加宽算子及变窄算子外，还怎么去计算近似它的最小不动点？这时伽罗瓦连接就派上用场了，先将L对应到另一个完全格M，即构造一个Galois连接或插入（L, α, γ, M），设A是L上的广义单调框架（不要求L满足升链条件，指定传递函数集合F为L到L的单调函数空间，即F本身也是完全格），其中f是L到L的单调函数，B是M上的广义单调框架，其中g是M到M的单调函数，保证g是由f衍生的函数的上近似即α◦f◦γ ⊑ g，及M满足升链条件。到了这里可以证明两个结论：
➀ lfp(f) ⊑ γ(lfp(g)) 和 α(lfp(f)) ⊑ lfp(g)
➁B的约束解(B₁, B₂)蕴含A的约束解(A₁, A₂)=(γ◦B₁, γ◦B₂)，下标1、2表示流图结点的入口、出口。接下来有两种方法可以计算近似L的最小不动点
1. 直接计算M上的最小不动点，然后应用上述结论➀，取lfp(f) = γ(lfp(g))
2. 构造M的上界算子（针对Galois连接）或加宽算子（针对Galois插入），满足 l₁ ∇ₗ l₂ = γ(α(l₁) ∇ₘ α(l₂))，可以证明左式为L上的一个加宽算子，取其lfp∇ₗ (f)。如果前面构造的是Galois插入，那么可以证明L和M两者的加宽算子精度是一样的，即lfp∇ₗ (f) = γ(lfp∇ₘ(α◦f◦γ ))
posted on 2023-09-06 22:42
春秋十二月 阅读(257)
评论(0) 编辑 收藏 引用 所属分类:
Compiler