[mercury-users] Newbie problem. :)

[Richard A. O'Keefe]

I suggested:

	> Given the clause
	>     :- p(X), q(X).
	> "p(X) and q(X) cannot both be true", then
	> a disjunction
	>     ( ... p(T) ... ; ... q(T) ... )
	> in a mode where T is ground can be compiled as
	> an if-then-else.
	
Peter Schachte replied:

	But for determinism, you also need to know that
	
		p(X) ; q(X).
	
True.  But for many cases of interest that _won't_ be true.
The classic example is numeric comparison.  In IEEE 754
floating point arithmetic (supported by M68k, M88k, PowerPC,
SPARC, Alpha, MIPS, 80*86/Pentium, &c), the negative clause


    :- X >= Y, X < Y  %where% float(X), float(Y).

*is* true, but the disjunction

    X >= Y ; X < Y %where% float(X), float(Y).

is *false*.  A precicate such as

    :- pred max(float, float, float).
    :- mode max(in, in, out).

    max(X, Y, Max) :- ( X >= Y -> Max = X ; X < Y, Max = Y ).

is *not* det, it is semidet.  And this was the case I was considering.
Note that if you want to conclude that max/3 written as above is det,
you *do* need to know that the disjunction is true, but you *don't*
need to know that the negative rule is true.

Some of you may be scratching your heads over this, but IEEE floating
point arithmetic, the kind of floating point arithmetic we have to
live with on most of the machines Mercury is likely to be used on,
has a class of values called NaNs, which do not compare less than,
greater than, or equal to anything at all; they don't even compare
equal to themselves.  Thus max(0.0/0.0, 0.0) will, and *should*,
fail.

	I think it would be better to allow declarations something like
	
		:- assertion p(X) <=> \+ q(X).
	
I agree that it would be *useful* to allow such declarations *as well*,
but it is important that people understand that there are *two* properties
involved:
    - at least one of p(X), q(X) must be true (the disjunction)
    - at most one of p(X), q(X) may be true (the negative rule)
and that these properties are independent.

	Since exclusive or would be a lot more natural for this, maybe the
	syntax should be
	
		:- assertion p(X) ! q(X).
	
At this stage, the syntax is not an issue.  The semantics _is_.

I also had in mind predicates as a replacement for patterns.
One of the serious weaknesses of Prolog, which Mercury has inherited,
is that you can give a name to a goal, but you can't give a name to
a pattern, so it is notably harder to use abstract data types than
to use concrete data types.  In particular, if you have something
like

    :- mode p(in, ...)
    p(foo(...), ...) :- ...
    p(bar(...), ...) :- ...

then the compiler can tell that these clauses are mutually exclusive,
*regardless of whether the predicate can or is intended to fail*, but
if those patterns are hidden inside predicates (as they have to be if
you seriously want to support abstract data types) then the compiler
can *not* tell that

    p(X, ...) :- foo(X), ...
    p(X, ...) :- bar(X), ...

has two mutually exclusive clauses.  To better support abstract data
types, I think it should be possible to _tell_ the compiler that
certain predicates are mutually incompatible.  Whether they form an
_exhaustive_ classification is a separate (but important) issue.

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