Exercises 6
Exercise 1 (Galois Connection). Remember that a Galois connection is defined by two monotonic functions α : C → A and γ : A → C between partial orders ≤ on C and ⊑ on A, such that
∀a,c. α(c) ⊑ a ⇐⇒ c ≤ γ(a) (∗)
a) Show that the condition (∗) is equivalent to the conjunction of these two conditions:
∀c. c ≤ γ(α(c))
∀a. α(γ(a)) ⊑ a
b) Let α and γ satisfy the condition of a Galois connection. Show that the following three conditions are equivalent:
1. α(γ(a)) = a for all a
2. α is a surjective function
3. γ is an injective function
c) State the condition for c = γ(α(c)) to hold for all c. When C is the set of sets of concrete states and A is a domain of static analysis, is it more reasonable to expect that c = γ(α(c)) or α(γ(a)) = a to be satisfied, and why?
Exercise 2 (lub and glb). Let (A,⊑) be a partial order such that every set S ⊆ A has the greatest lower bound.
Prove that then every set S ⊆ A has the least upper bound, or show a
counterexample.
What about the lattice with three elements {0,1a,1b} the relations 0 ≤ 1a and 0 ≤ 1b?
1
Exercise 3 (Lattices). Consider algebraic structures with signature (∨,∧), each of arity 2, and satisfying the following axioms:
x ∨ y = y ∨ x
(x ∨ y) ∨ z = x ∨ (y ∨ z) x ∨ x = x x ∨ (x ∧ y) = x x ∧ y = y ∧ x
(x ∧ y) ∧ z = x ∧ (y ∧ z) x ∧ x = x x ∧ (x ∨ y) = x
a) Show that for any x and y, x ∧ y = x if and only if x ∨ y = y.
b) Define x ≤ y by x ∧ y = x. Show that ≤ is a partial order relation.
c) Show that ∧ and ∨ are respectively the binary greatest lower bound and least upper bound for ≤.
Exercise 4 (post). let S be any set, r ⊆ S ×S a binary relation and I ⊆ S. Define post : 2S → 2S by post(X) = I ∪ r[X]. Prove that post is monotonic. Does post admit a least fixed point?
Exercise 5. Partitioning
a) Show that for any set ) is a lattice.
b) Consider a set S = P × V . For each set g ∈ 2P×V , define ¯g : P → 2V by ¯g(p) = {v | (p,v) ∈ g}. Show that the bar function ¯· defines a bijection between 2P×V and P → 2V .
c) Consider the set of all functions P → 2V . Define a lattice on this set that is isomorphic to (2P×V ,⊆).
Remember: A lattice isomorphism between two lattices L1 and L2 is a bijective function f : L1 → L2 such that f(x ∧ y) = f(x) ∧ f(y), f(x ∨ y) = f(x) ∨ f(y) and f(x) ≤ f(y) holds if and only if x ≤ y.
2
