[m-rev.] for review: comparison preds/funcs

[Mark Brown]

On 13-Sep-2002, Fergus Henderson <fjh at cs.mu.OZ.AU> wrote:
> On 13-Sep-2002, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> > @@ -166,6 +170,7 @@
> > +++ library/builtin.m	12 Sep 2002 06:43:08 -0000
> > +	% Values of types comparison_pred/1 and comparison_func/1 are used
> > +	% by predicates and functions which depend on an ordering on a given
> > +	% type, where this ordering is not necessarily the standard ordering.
> > +	% In addition to the type, mode and determinism constraints, a
> > +	% comparison predicate C is expected to obey two other laws.  For
> > +	% all X, Y and Z of the appropriate type, and for all
> > +	% comparison_results R:
> > +	%	1) C(X, Y, (>)) if and only if C(Y, X, (<))
> > +	%	2) C(X, Y, R) and C(Y, Z, R) implies C(X, Z, R).
> 
> I suggest mentioning the names of these laws (symmetry and
> transitivity), e.g. by s/1)/(symmetry)/ and s/2)/(transitivity)/

It is not immediately obvious, since our presentation differs from the
usual, but the first rule is actually not the same as antisymmetry.  It
is similar---it says that the ordering on the _equivalence_classes_ of
elements is antisymmetric---but is not as strong as saying that the
ordering on elements themselves is antisymmetric.

Note that the above constraints do imply reflexivity (that is, C(X, X, (=)))
and linearity (that is, all pairs are comparable), and rule 2 is transitivity,
so if we also had antisymmetry then we would have a total order -- which is
precisely the constraint we started with.

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-reviews mailing list
post:  mercury-reviews at cs.mu.oz.au
administrative address: owner-mercury-reviews at cs.mu.oz.au
unsubscribe: Address: mercury-reviews-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-reviews-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------