Partial vs. strict weak ordering (was Re: [PATCH] Postinstall script ordering in setup - take 3)

[Igor Pechtchanski <pechtcha at cs dot nyu dot edu>]

On 16 Mar 2003, Robert Collins wrote:

> On Sat, 2003-03-15 at 09:33, Igor Pechtchanski wrote:
> > Rob,
> > > Your operator > and < appear to have a problem.
> > >
> > > foo: bar
> > > gam: bar
> > >
> > > foo > gam    = false
> > > gam < foo    = false
> > > gam == foo   = false.
> > >
> > > I'd expect stl associative containers to choke on that.
>
> > Not really.  I read up on that specifically.  stl containers only need a
> > *partial* order.  What you're suggesting will create a total order.  Not
> > an error, but overkill.  The sort function is supposed to be stable and
> > keep the original order if the lessThan relation is undefined.  See
> > <http://www.sgi.com/tech/stl/LessThanComparable.html>
>
> =================
>
> Consider the relation !(x < y) && !(y < x). If this relation is
> transitive (that is, if !(x < y) && !(y < x) && !(y < z) && !(z < y)
> implies !(x < z) && !(z < x)), then it satisfies the mathematical
> definition of an equivalence relation. In this case, operator< is a
> strict weak ordering.
>
> If operator< is a strict weak ordering, and if each equivalence class
> has only a single element, then operator< is a total ordering.
>
> Valid expressions
>        Name
>     Expression
> Type requirements
>    Return type
> Less
> x < y
>
> Convertible to
> bool
> Greater
> x > y
>
> Convertible to
> bool
> Less or equal
> x <= y
>
> Convertible to
> bool
> Greater or equal
> x >= y
>
> Convertible to
> bool
> Expression semantics
>      Name
>   Expression
>  Precondition
>   Semantics
> Postcondition
> Less
> x < y
> x and y are in
> the domain of
> <
>
> Greater
> x > y
> x and y are in
> the domain of
> <
> Equivalent to
> y < x [1]
>
> Less or equal
> x <= y
> x and y are in
> the domain of
> <
> Equivalent to
> !(y < x) [1]
>
> Greater or
> equal
> x >= y
> x and y are in
> the domain of
> <
> Equivalent to
> !(x < y) [1]
>
> Complexity guarantees
> Invariants
> Irreflexivity
> x < x must be false.
> Antisymmetry
> x < y implies !(y < x) [2]
> Transitivity
> x < y and y < z implies x < z [3]
> Models
>       * int
>
> Notes
> [1] Only operator< is fundamental; the other inequality operators are
> essentially syntactic sugar.
>
> [2] Antisymmetry is a theorem, not an axiom: it follows from
> irreflexivity and transitivity.
>
> [3] Because of irreflexivity and transitivity, operator< always
> satisfies the definition of a partial ordering. The definition of a
> strict weak ordering is stricter, and the definition of a total ordering
> is stricter still.
> =================
> foo: bar
> gam: bar
>
> gives
>
> foo > bar
> gam > bar
> from above:
> Axiom: ! (foo < gam) && (! gam < foo)
> Axiom: ! (foo < gam) && (! gam < foo) && !(gam < z) && !(z < gam)
> is
> !(foo < z) && (!z < foo)
> ever false?
> now, foo is < z when z depends on foo. !(foo < z) means z does not
> depend on foo.
> what do we know about z?
> z does not depend on gam. !(gam < z)
> gam does not depend on z  !(z < gam)
> can z depend on foo and not on gam?
> let z depend on foo:
> so: z > foo.
>
> now, !(gam < z) is still true. !(z < gam) is still true.
> !(foo < z) is false.

Yes.  It reads better this way: !(x < y) && !(y < x) === unordered(x,y)
Reflexivity: unordered(x,x)
Transitivity: unordered(x,y) && unordered(y,z) => unordered(x,z)

And I agree that "unordered(x,y)" defined in terms of my operator< is
*not* transitive.  Thus, my operator< is not a strict weak ordering.  It
*is*, however, a partial ordering (see note [3] above).

> Your operator < is not a equivalence relation.

Now, operator< is *never* an equivalence relation (because it's
irreflexive, rather than reflexive).  My operator< *is* transitive,
because of the "propagateDependences" step...

> STL Containers will choke.
> You fail on transitivity BTW.
> Rob

STL containers won't choke, as they only need a partial order, AFAIU.
The "fail" simply means it's not a strict weak ordering.

Now, what my operator< *does* fail on is irreflexivity (in case there are
circular dependences).  I'll need to fix that (it's a TODO).
	Igor
-- 
				http://cs.nyu.edu/~pechtcha/
      |\      _,,,---,,_		pechtcha at cs dot nyu dot edu
ZZZzz /,`.-'`'    -.  ;-;;,_		igor at watson dot ibm dot com
     |,4-  ) )-,_. ,\ (  `'-'		Igor Pechtchanski
    '---''(_/--'  `-'\_) fL	a.k.a JaguaR-R-R-r-r-r-.-.-.  Meow!

Oh, boy, virtual memory! Now I'm gonna make myself a really *big* RAMdisk!
  -- /usr/games/fortune