Program Analysis - Exercise Sheet 5 March 2015 Let (L1 , v1 , t1 , u1 ) and (L2 , v2 , t2 , u2 ) be two complete lattices. Exercise 1 Can you find an example where: – α : L1 ⇒ L2 is completely join-preserving – γ : L2 ⇒ L1 is completely meet-preserving – γ ◦ α is extensive yet (α, γ) does not form a Galois Connection ? Solution α ◦ γ is not reductive for y. Exercise 2 Give example of a Galois connection which is not a Galois insertion. 1 Solution γ is not injective. Exercise 3 • Given two monotone functions f : L1 → L1 and g : L2 → L2 and a Galois connection (α, γ) between L1 and L2 , prove that the following statements are equivalent: – ∀z ∈ L2 : α(f (γ(z))) v2 g(z) – ∀z ∈ L2 : f (γ(z)) v1 γ(g(z)) • If (α, γ) is not a Galois connection, show that the statements above are equivalent or give a counter-example. Solution • We prove the first statement implies the second one. "=>" Let us apply monotone function γ to the first statement: ∀z ∈ L2 : γ(α(f (γ(z)))) v1 γ(g(z)) By γ ◦ α extensive: ∀z ∈ L2 : f (γ(z)) v1 γ(α(f (γ(z)))) v1 γ(g(z)) "<=" By applying monotone function α to the second statement: ∀z ∈ L2 : α(f (γ(z))) v2 α(γ(g(z))) By α ◦ γ reductive: ∀z ∈ L2 : α(f (γ(z))) v2 α(γ(g(z))) v2 g(z) 2 • If (α, γ) is not a Galois connection, then the statements are not equivalent. It is sufficient to look at the example from Exercise 1, and define f and g as identity functions on L1 , respectively L2 . Exercise 4 Assume L2 = {⊥, >}, with ⊥v2 > and ∀e ∈ L1 : α(e) = >. Can you find γ such that (α, γ) is a Galois connection? Solution In this case, α is not completely join-preserving, thus we cannot build a Galois Connection using this α. We now show by contradiction why α is not completely join-preserving: We assume α is completely join-preserving. This means: ∀Y ⊆ L1 : α(tY ) = t{α(y)|y ∈ Y } Let us pick Y = ∅. By substitution, we obtain: α(t∅) = t{α(y)|y ∈ ∅} This is equivalent with: α(⊥1 ) = t∅ (⊥1 is the least element in L1 ) ≡ > =⊥ (⊥ is the least element in L2 ) We reached contradiction. This implies α is not completely join-preserving. 3

© Copyright 2020