[mercury-users] Re: Determinism detection (Was Newbie problem.)

[Richard A. O'Keefe]

	> Note that in general these things will have multiple
	> arguments, some output, so you need to be careful with quantifiers
	> (the examples given are simplistic in this respect).
	
	Yes.  Richard O'Keefe's and Peter Schachte's suggestions didn't
	discuss situations with multiple arguments.
	
Hang on, my primary example was "X >= Y" -vs- "X < Y" or something
like that.  Looks like multiple arguments to *me*.

There was a _reason_ why I cast my exclusion suggestion in the form
of negative rules:  they inherit a precise semantics from the normal
logic programming semantics of Horn clauses.

In fact the _general_ negative rule case is that if one disjunct
subsumes some of the goals in a negative rule, and another
disjunct subsomes the remaining goals, and the arguments in question
are ground (which Mercury knows when Prolog in general doesn't, which
is why this idea suits Mercury much better than it does Prolog), then
the first disjunction excludes the second and some sort of pruning
can be done after the last subsumed negative rule goal.

For example, suppose we want to say that there are no rich honest
politicians.  Then

    :- wealth(P, M), M > 200_000, honest(P), seat(P, X).

might do.  Then if we have a disjunction

    (  <1> wealth(Q, W), W >= 250_000, <a> ...W...
    ;  <2> honest(Q), seat(Q, X) <b> ...X..
    )

then reaching point <a> justifies pruning away disjunct <2>,
while reading point <b> justifies pruning away disjunct <1>.
No, there isn't a misprint:  I think "W >= 250_000" subsumes
"W >= 200_000".  And you have to know that wealth/2 and seat/2
are functional, which the Mercury mode system lets you say.


	In general I'm pretty supportive of their general approach, but
	I would like to see a more detailed and complete proposal.
	
So would I.  I think my proposal is sufficiently concrete.
That doesn't mean I think it can't be improved.
As Peter Schachte has clearly shown, it is _incomplete_.

Note that attaching this information to types is NOT going to work.
Why not?  Because this is one of the things that Ada and Lisp got
*right* and Eiffel got *wrong*:  a package may legitimately and
usefully declare more than one type inside the encapsulation boundary.
(C++ drills holes in the pressure hull, using 'friend', and Eiffel
has a close equivalent of `friend' that lets you control which
features are visible to which friends.)

For example, suppose I have the usual sort of linear algebra package
with a 'matrix' type and a 'vector' type.  Then I might want to know
whether a matrix and a vector conform in size or not.  So I might
have predicates

    vm_conformant(Vector, Matrix) % the product Vector +.x Matrix is ok
    vm_nonconformant(Vector, Matrix) % it isn't
    mv_conformant(Matrix, Vector) % the produce Matrix +.x Vector is ok
    mv_nonconformant(Matrix, Vector) % it isn't

with the obvious exclusive-or rules (while I think that pure negative
rules are often needed, Peter Schachte is right that exclusive-or
rules are also often needed):

    vm_conformant(V, M) # vm_nonconformant(V, M).
    mv_conformant(M, V) # mv_nonconformant(M, V).

Now, to which single type do these rules belong?

No, the obvious answer to "where does this information belong" is
"in the same place that _other_ information about these predicates
belongs".  This isn't information about *types*, it's information
about *predicates*.

--------------------------------------------------------------------------
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
--------------------------------------------------------------------------