<!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 < or <= in
PORDERED_CORE. I would go
<br>
for <. 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>
< or <=:
<br>
<br>
a < b a < b not (b <= a)
<br>
a > b b < a not (a <= b)
<br>
a <= b not (b < a) a <= b
<br>
a >= b not (a < b) b <= a
<br>
a == b not (a < b or b < a) a <= b and b
<= a
<br>
a != b a < b or b < a not (a <= b and b
<= a)
<br>
<br>
A semi-technical reason would be that < is one character shorter
than <=
<br>
and definitions using < 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 <= = Set.isSubset<br>
<br>
instead of <br>
<br>
fun x < y = Set.isSubset (x, y) andalso not (Set.==(x, y))<br>
<br>
furthermore in some cases equality will be defined in terms of <=
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>