<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
  <meta content="text/html;charset=UTF-8" http-equiv="Content-Type">
</head>
<body bgcolor="#ffffee" text="#000000">
Vesa Karvonen wrote:<br>
<blockquote
 cite="mid:9e43b9a0705031347n45661c16n2956c920fd9c0e51@mail.gmail.com"
 type="cite">I'm not sure whether one should use &lt; or &lt;= in
PORDERED_CORE.  I would go
  <br>
for &lt;.  This is probably mostly because that is what I got used to
when
  <br>
working with the C++ STL.  I don't know if there is any technical
reason
  <br>
to prefer one over the other.  In particular, it takes on average the
same
  <br>
number of operations to synthesize other relational operators from
either
  <br>
&lt; or &lt;=:
  <br>
  <br>
 a &lt; b              a &lt; b                 not (b &lt;= a)
  <br>
 a &gt; b              b &lt; a                 not (a &lt;= b)
  <br>
 a &lt;= b        not (b &lt; a)                     a &lt;= b
  <br>
 a &gt;= b        not (a &lt; b)                     b &lt;= a
  <br>
 a == b        not (a &lt; b or b &lt; a)            a &lt;= b and b
&lt;= a
  <br>
 a != b             a &lt; b or b &lt; a        not (a &lt;= b and b
&lt;= a)
  <br>
  <br>
A semi-technical reason would be that &lt; is one character shorter
than &lt;=
  <br>
and definitions using &lt; therefore lead to a few characters shorter
code.
  <br>
All other things being equal, shorter is better.
  <br>
</blockquote>
    While shorter is usually better, I'm not sure I agree in this
case.  At least I hypothesize that most times that someone would want
to define a partial order, they would find it more natural to define it
in terms of a reflexive, transitive, anti-symmetric relation, rather
than a transitive, anti-symmetric relation.  For example, in one of my
several structures that admits a partial order (but not a total order)
is an ordering based upon subset inclusion.  Therefore, I could define <br>
<br>
    val op &lt;= = Set.isSubset<br>
<br>
instead of <br>
<br>
    fun x &lt; y = Set.isSubset (x, y) andalso not (Set.==(x, y))<br>
<br>
furthermore in some cases equality will be defined in terms of &lt;=
and therefore writing something like the above may be a little awkward.<br>
<br>
<br>
<pre class="moz-signature" cols="72">-- 
[Geoff Washburn|<a class="moz-txt-link-abbreviated" href="mailto:geoffw@cis.upenn.edu">geoffw@cis.upenn.edu</a>|<a class="moz-txt-link-freetext" href="http://www.cis.upenn.edu/~geoffw/">http://www.cis.upenn.edu/~geoffw/</a>]
</pre>
</body>
</html>