On 11/20/2014 03:12 AM, Waldek Hebisch wrote: > For PartialOrder we do not assume existence of equality > and in cases where we have equality we do not assume that 'x <= y' > and 'y <= x' imply 'x = y' (so our is most general definition of > partial order appearing in litarature).
Ooops. If antisymmetry is not assumed, then my background tells me to call this quasiorder or preorder, but not partial order. http://en.wikipedia.org/wiki/Partially_ordered_set Can you give a reference to "the literature". (I actually believe that some people call a (ir)reflexive and transitive relation "partial order", but I don't recall that I have ever seen this in a book.) Oh... I just see this... https://github.com/fricas/fricas/blob/master/src/algebra/catdef.spad#L1179 )abbrev category PORDER PartialOrder ++ Author: Waldek Hebisch ++ Description: ++ The class of partially ordered sets, that is sets equipped with ++ transitive and reflexive relation \spad{<=}. PartialOrder() : Category == with "<": (%,%) -> Boolean ++ x < y is a less than test. ">": (%, %) -> Boolean ++ x > y is a greater than test. ">=": (%, %) -> Boolean ++ x >= y is a greater than or equal test. "<=": (%, %) -> Boolean ++ x <= y is a less than or equal test. add x >= y == y <= x x > y == y < x x < y == x <= y and not(y <= x) Without the axiom of asymmetry a<b ==> ~(b<a) and antisymmetry (a<=b /\ b<=a) ==> a=b for < and <=, respectively, I wouldn't call that a "partial order", but rather only a quasiorder. Can we agree on renaming your PartialOrder to PreOrder or QuasiOrder and introducing a PartialOrder category that has the asymmetry/antisymmetry required? Since antisymmetry requires "=", one might even want to split into irreflexive and reflexive partial order. ++ irreflexive, asymmetric, transitive relation IrreflexivePartialOrder: Category == with _<: (%,%) -> Boolean _>: (%, %) -> Boolean add x > y == y < x ++ reflexive, antisymmetric, transitive relation ReflexivePartialOrder: Category == BasicType with _<=: (%,%) -> Boolean _>=: (%, %) -> Boolean add x >= y == y <= x PartialOrder: Category == Join( IrreflexivePartialOrder, ReflexivePartialOrder) add x <= y == x < y or x = y Admittedly, joining something irreflexive with something reflexive looks strange, but the operations are disjoint and maybe one can find better names. Ralf -- You received this message because you are subscribed to the Google Groups "FriCAS - computer algebra system" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To post to this group, send email to [email protected]. Visit this group at http://groups.google.com/group/fricas-devel. For more options, visit https://groups.google.com/d/optout.
