Remarks and Questions on the Monotone Framework
In the Monotone Framework (Module 2, slide 68) we assume a complete lattice
where each subset of L has a least upper bound and a greatest lower bound (slide 52).
In the presented analyses (slides 73ff) we only use finite sets (like the power set of all variables resp. nontrivial subexpressions occurring in the program). Hence I think it suffices to assume that just finite subsets have a least upper bound resp. a greatest lower bound.
We also use only the least upper bound, not the greatest lower bound.
(In the Available Expressions Analysis for example, we use therefore the "dual lattice" (slide 74).)
So I think we do not really need a lattice, but it suffices to assume a (join-)semilattice.
On slide 80 we use three dimensions (powerset lattice/dual powerset lattice, forward/backward and smallest/largest solution) to characterize instances of the Monotone Framework. Does it not depend on the choice of the powerset/dual powerset lattice, whether one looks for the smallest or the largest solution? If we use the powerset lattice (May Analyses, where we take the Union of the neighbor solutions) we are looking for the smallest solution (slide 38) (since the whole set of variables trivially solves the equation). If we use the dual power set lattice (Must Analyses, where we take the Intersection of the neighbor solutions) we are looking for the largest solution (slide 32) (since the empty set trivially solves the equation). So are this actually not three dimensions, but two?