Lab for Automated Reasoning and Analysis LARA

Homework 03: Due April 16

Problem 1

Let ${\cal F}$ be the set of all first-order formulas (viewed as syntax trees, so e.g. $(x \land y)$ is a different formula from $(y \land x$) and let $r$ be the implication relation on formulas:

   r = \{ (F_1,F_2) \mid \models F_1 \rightarrow F_2 \}

Check whether $r$ is reflexive, antisymmetric, and transitive relation.

Problem 2

Let $(A,\sqsubseteq)$ be a partial order such that every set $S \subseteq A$ has the greatest lower bound. Prove that then every set $S \subseteq A$ has the least upper bound.

Problem 3

Galois connection is defined by two monotonic functions $\alpha : C \to A$ and $\gamma : A \to C$ between partial orders $\leq$ on $C$ and $\sqsubseteq$ on $A$, such that

  \alpha(c) \sqsubseteq a\ \iff\ c \leq \gamma(a) \qquad (*)

for all $c$ and $a$ (intuitively, the condition means that $c$ is approximated by $a$).

Part a) Show that the condition $(*)$ is equivalent to the conjunction of these two conditions:

  c &\leq& \gamma(\alpha(c)) \\
  \alpha(\gamma(a)) &\sqsubseteq& a

hold for all $c$ and $a$.

Part b) Let $\alpha$ and $\gamma$ satisfy the condition of Galois connection. Show that the following three conditions are equivalent:

Problem 4

Consider Problem 3 on the Space of Invariants in the previous homework, Homework 02.

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

b): From now on, fix the relation $r$. Define $\alpha(I) = sp(I,r)$ and define $g(I) = wp(r,I)$. Are functions $f$ and $g$ monotonic? Do they form a Galois connection? Prove or give a counterexample.

c): For each of the functions $f$, $g$, describe the space of prefix points, postfix points, as well as the least and the greatest fixpoints. You may find Fixed Point Theorems useful.

sav10/homework_03.txt · Last modified: 2015/04/21 17:34 (external edit)