【性質】
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插入。獨立特征、直積、約化積與其它方法的區(qū)別是兩對抽象化函數與具體化函數之間沒有相互作用，會損失分析結果精度，本質就是P(A)×P(B)和P(A×B)的差別（P為冪集，A、B為集合）；獨立特征與直積、約化積的區(qū)別是具體化函數定義不同（抽象化函數相同），前者是兩個具體化函數的二元組即γ(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
春秋十二月 閱讀(297)
評論(0) 編輯 收藏 引用 所屬分類:
Compiler