Space of Invariants

Problem Statement

Let be a set (e.g. the set of all integers). Let and . Define

For each element we have and we think of as an invariant.

Prove each of the following statements or give a counterexample.

a): If , then .

b): The set is finite.

c): If then also .

d): If then also .

e): Let and let

in other words, by definition of ,

Prove that then . What do we obtain for ?

f): Let and let

in other words, by definition of ,

Prove that then . What do we obtain for ?

g): Is the set a lattice? If it is a lattice, is it complete? If it is not a lattice, can it be modified to become a lattice?

Solutions

Solution a)

True.

First we prove the following lemme using induction on .

Lemma

Base. Assume .

We show .

This holds according to the definition of invariants.

Inductive step. Assume . We show .

By the induction assumption we know .

We can easily show for two invariants and that . This proves the lemma.

From the lemma we can conclude .

The set is non-empty, so there exists such that . This shows that .

Solution b)

False.

You can easily find counter-examples.

Solution c,d)

Both true.

The assumption gives us the following.

From the set theory we know that if and then we can conclude both and .

We can use this fact on the on the corresponding components:

Computing the union gives us:

Due of the disjunctivity of we can conclude that is an invariant.

For the intersection case we replace the invariant of with a stronger one . Similarly for .

This can be done due to the monotonicity of .

The proof is similar to the union case.

Solution e)

Consider the following equivalence.

We show that each conjunct is valid.

• . Holds since is included in every invariant.

Let be an arbitrary member of .

Nested quantifiers can be swapped, but the reverse does not necessarily hold.

• . Holds if is non-empty.

If and we claim .

We proved in (a) that . It remains to prove the other two conditions.

Which shows that is included in .

This is correct because

To prove that is the bottom element we have to prove the following.

Which was proved in a lemma in part (a).

Solution f)

Consider the following equivalence.

We show that each conjunct is valid.

• . Holds since is included in every invariant.

Let be an arbitrary member of .

• . Holds if is non-empty.

If and we claim .

To prove that is the top element we have to prove the following.

We prove the following lemme using induction on .

Base. Assume .

We show .

This holds according to the definition of invariants.

Inductive step. Assume . We show .

By the induction assumption we know .

We can also easily show for two invariants and that . Note that the condition is equivalent to .

This proves the lemma.

Solution g)

The ordered set is a lattice. We proved in part (c ) and (d) that for any both and exist and are equal to and respectively.

We showed in part (e) and (f) that for every subset both lub and gub exist: and .

The lattice is complete. The top element is and the bottom element is .