【性質】
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
春秋十二月 閱讀(275)
評論(0) 編輯 收藏 引用 所屬分類:
Compiler