【性質(zhì)】
1. 判定兩個(gè)完全格L和M能否構(gòu)成伽羅瓦連接，即抽象化函數(shù)α: L—>M是否完全加性的，或具體化函數(shù)γ: M—>L是否完全乘性的
2. 構(gòu)造抽象化函數(shù)和具體化函數(shù)，即對(duì)于一個(gè)Galois連接（L, α, γ, M），給定α可通過γ(m) = ⊔{l | α(l) ⊑ m}確定γ，這對(duì)于所有m成立，且由于α是確定的，因此γ是唯一確定的。取最小上界是為了保證m描述的L中元素對(duì)于所有安全地描述了M中α(l)的l是安全的；給定γ可通過 α(l) = ⊓ {m | l ⊑ γ(m) } 確定α，其唯一性和取最大下界的原因類似前面
3. 幫助定義分析具體格源值到抽象格屬性的正確性關(guān)系與表示函數(shù)。設(shè)有Galois連接（L, α, γ, M），R: V×L —>{true, false}為正確性關(guān)系，由表示函數(shù)β:V—>L生成，定義S: V×M —>{true, false}，則有v S m ⇔ v R (γ(m)) ⇔ β(v ) ⊑ γ(m) ⇔ (α◦β)(v) ⊑ m，即S為正確性關(guān)系，由表示函數(shù)α◦β: V—>M生成
4. 抽象化上迭代多次具體化+抽象化，結(jié)果等于一次抽象化，即α◦γ◦α = α；具體化上迭代多次抽象化+具體化，結(jié)果等于一次具體化，即γ◦α◦ γ = γ。這個(gè)性質(zhì)被用于基于約化算子構(gòu)造的伽羅瓦插入（特殊的伽羅瓦連接：具體化為單射，抽象化為滿射）的證明
【組合】
分三大類，即順序組合、并行組合和函數(shù)空間。為簡(jiǎn)化描述，下文簡(jiǎn)稱Galois為G
1. 順序組合：取第一個(gè)G連接的具體格，最后一個(gè)G連接的抽象格，從第一個(gè)G連接到最后一個(gè)G連接組合各抽象化函數(shù)，從最后一個(gè)G連接到第一個(gè)G連接組合各具體化函數(shù)。例如，設(shè)（L₀, α₁, γ₁, L₁）和（L₁, α₂, γ₂, L₂）都是G連接，則（L₀, α₂◦α₁, γ₂◦γ₁, L₂）也是一個(gè)G連接
2. 并行組合：有六種方法，即獨(dú)立特征、相關(guān)性、直積、直張量積、約化積、約化張量積，前兩種用于組合分別針對(duì)不同結(jié)構(gòu)多個(gè)分析的多個(gè)G連接為一個(gè)G連接。中間兩種組合針對(duì)同一結(jié)構(gòu)多個(gè)分析的多個(gè)G連接為一個(gè)G連接，后兩種組合針對(duì)同一結(jié)構(gòu)多個(gè)分析的多個(gè)G連接為一個(gè)G插入。獨(dú)立特征、直積、約化積與其它方法的區(qū)別是兩對(duì)抽象化函數(shù)與具體化函數(shù)之間沒有相互作用，會(huì)損失分析結(jié)果精度，本質(zhì)就是P(A)×P(B)和P(A×B)的差別（P為冪集，A、B為集合）；獨(dú)立特征與直積、約化積的區(qū)別是具體化函數(shù)定義不同（抽象化函數(shù)相同），前者是兩個(gè)具體化函數(shù)的二元組即γ(m₁, m₂)=(γ₁(m₁), γ₂(m₂))，后者則是最大下界即γ(m)=γ₁(m₁)∧γ₂(m₂)
3. 函數(shù)空間：分為總函數(shù)空間和單調(diào)函數(shù)空間。對(duì)于前者，設(shè)（L, α, γ, M）為一個(gè)G連接，S為一個(gè)集合，f為S到L的函數(shù)，g為S到M的函數(shù)，因L和M為完全格，故由f或g構(gòu)成的函數(shù)集合為總函數(shù)空間，則得到一個(gè)G連接（S—>L, α', γ', S—>M），其中α'(f)=α◦f, γ'(g)=γ◦g。對(duì)于后者，設(shè)（L₁, α₁, γ₁, M₁）和（L₂, α₂, γ₂, M₂）為G連接，f為L(zhǎng)₁到L₂的函數(shù)，g為M₁到M₂的函數(shù)，因每個(gè)L及M為完全格，故由f或g構(gòu)成的函數(shù)集合為單調(diào)函數(shù)空間，則得到一個(gè)G連接（L₁—>L₂, α, γ, M₁—>M₂），其中α(f)=α₂ ◦f ◦γ₁，γ(g)=γ₂◦ g◦ α₁
【應(yīng)用】
當(dāng)要做數(shù)據(jù)流分析的一個(gè)完全格L不滿足升鏈條件時(shí)，除了直接對(duì)L運(yùn)用加寬算子及變窄算子外，還怎么去計(jì)算近似它的最小不動(dòng)點(diǎn)？這時(shí)伽羅瓦連接就派上用場(chǎng)了，先將L對(duì)應(yīng)到另一個(gè)完全格M，即構(gòu)造一個(gè)Galois連接或插入（L, α, γ, M），設(shè)A是L上的廣義單調(diào)框架（不要求L滿足升鏈條件，指定傳遞函數(shù)集合F為L(zhǎng)到L的單調(diào)函數(shù)空間，即F本身也是完全格），其中f是L到L的單調(diào)函數(shù)，B是M上的廣義單調(diào)框架，其中g(shù)是M到M的單調(diào)函數(shù)，保證g是由f衍生的函數(shù)的上近似即α◦f◦γ ⊑ g，及M滿足升鏈條件。到了這里可以證明兩個(gè)結(jié)論：
? lfp(f) ⊑ γ(lfp(g)) 和 α(lfp(f)) ⊑ lfp(g)
?B的約束解(B₁, B₂)蘊(yùn)含A的約束解(A₁, A₂)=(γ◦B₁, γ◦B₂)，下標(biāo)1、2表示流圖結(jié)點(diǎn)的入口、出口。接下來有兩種方法可以計(jì)算近似L的最小不動(dòng)點(diǎn)
1. 直接計(jì)算M上的最小不動(dòng)點(diǎn)，然后應(yīng)用上述結(jié)論?，取lfp(f) = γ(lfp(g))
2. 構(gòu)造M的上界算子（針對(duì)Galois連接）或加寬算子（針對(duì)Galois插入），滿足 l₁ ∇ₗ l₂ = γ(α(l₁) ∇ₘ α(l₂))，可以證明左式為L(zhǎng)上的一個(gè)加寬算子，取其lfp∇ₗ (f)。如果前面構(gòu)造的是Galois插入，那么可以證明L和M兩者的加寬算子精度是一樣的，即lfp∇ₗ (f) = γ(lfp∇ₘ(α◦f◦γ ))
posted on 2023-09-06 22:42
春秋十二月 閱讀(275)
評(píng)論(0) 編輯 收藏 引用 所屬分類:
Compiler