On Mon, Nov 04, 2013 at 11:29:46AM -0800, Felix S Klock II wrote:
> > +Based on this lattice, the solution V(A)=+, V(B)=-, V(C)=o is the
> > +minimal solution (which is what we are looking for; the maximal
> > +solution is just that all variables are invariant. Not so exciting.).
> 
> How sure are you that you don't have the words "minimal" and "maximal" switched here?

I think I have it backwards, indeed. The phrase "least upper bound"
implies that the top of the lattice is greater. Obviously this is
rather arbitrary. I think part of it is that I initially framed the
lattice in the opposite way -- as a result of misreading the paper's
notation and using `o` for bivariant and `*` for invariant. When I
fixed this, I tried to convert all minimals to maximals and vice
versa, but I probably missed some. Regardless, a better idea would be
to eschew words like "minimal" and "maximal" in favor of something
clearer, like "best" vs "naive" solution or something similar.