Take the 2-minute tour ×
Mathematics Stack Exchange is a question and answer site for people studying math at any level and professionals in related fields. It's 100% free, no registration required.

I'm reading this paper: http://www.lsi.upc.edu/~albert/papers/handbook.ps.gz

and I can't understand a part of it. it defines an ordering on multisets (it defines a multiset over $A$ as a function $A \rightarrow N$)

and says (page 13) multisets are ordered by the smallest irreflexive, transitive relation $\succ\succ$ such that $M \cup \{s\} \succ\succ N \cup \{t_1,\ldots,t_n\} \; \mbox{if} \; M==N \land s \succ t_i \; \forall i \in 1 \ldots n$

but later it says (page 24) $\{s, t\} \succ\succ \{u, v\}$ if $\\s > u \land (s \geq v \lor t \geq v) \;\lor\; s > v \land (s \geq u \lor t \geq u) \;\lor\\ t > u \land (s \geq v \lor t \geq v) \;\lor\; t > v \land (s \geq u \lor t \geq u)$

(by page 15, $>$ and $=$ are interpreted as a given total (up to $=_c$)reduction ordering $\succ$ and congruence $=_c$ respectively)

which would seem to make $\succ\succ$ not aymmetric, but it must be asymmetric as it is transitive and irreflexive

the problem is that it could be the case that $s > u \land s = v$ which would make $\{s, t\}$ greater but also $v > t \land s = v$ which would make $\{u, v\}$ greater if we apply the rule backwards

I guess it might be the case that this rule only works because of constraints on the multisets

The way the E theorem prover computes this seems to make sense:

  int LiteralCompareFun(Eqn_p lit1, Eqn_p lit2)
     int cmpres;

     if(EqnIsPositive(lit1) && !EqnIsPositive(lit2))
        return 1;
     else if(!EqnIsPositive(lit1) && EqnIsPositive(lit2))
        return -1;
     cmpres = PCmp(MAX(lit1->lterm, lit1->rterm), 
           MAX(lit2->lterm, lit2->rterm));

        return cmpres;
     return PCmp(MIN(lit1->lterm, lit1->rterm), 
             MIN(lit2->lterm, lit2->rterm));
share|improve this question
You’ve inverted every order from p. 13, and you’ve transcribed the constraints on p. 24 incorrectly: they involve the binary predicate symbol $>$, defined on p. 15, which is not the same as $\succ$. –  Brian M. Scott Jul 11 '12 at 9:10
I think I fixed the problems –  Emma Jul 11 '12 at 9:30
add comment

Your Answer


By posting your answer, you agree to the privacy policy and terms of service.

Browse other questions tagged or ask your own question.