2
$\begingroup$

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));       if(cmpres)      {         return cmpres;      }      return PCmp(MIN(lit1->lterm, lit1->rterm),               MIN(lit2->lterm, lit2->rterm));   } 
  • 0
    I think I fi$x$ed the problems2012-07-11

0 Answers 0