[mercury-users] Determinism detection for different notations.

[Ralph Becket]

Bartlomiej Szymczak, Thursday, 31 May 2007:
> Hi.
> 
> Consider the following excerpt from my code:
> 
> :-pred uselessWord(string::in) is semidet.
> 
> uselessWord("a").
> uselessWord("her").
> 
> :-type yesno ---> yes ; no.
> 
> :-pred isu(string::in,yesno::out) is det.
> isu(W,X):-(if uselessWord(W) then X=yes else X=no).
> 
> This code works and compiles OK. However, I find the syntax very ugly,
> so at first I was trying more FOL-like notation for isu
> predicate:
> 
> :-pred isu(string::in,yesno::out) is det.
> isu(W,yes):-uselessWord(W).
> isu(W,no):- \+uselessWord(W).
> 
> But with such a definition, I get a compiler error:
> 
> john.m:140: In `isu(in, out)':
> john.m:140:   error: determinism declaration not satisfied.
> john.m:140:   Declared `det', inferred `nondet'.
> john.m:141:   call to `john.uselessWord(in)' can fail.
> john.m:142:   Negated goal can succeed.
> john.m:141:   Disjunction has multiple clauses with solutions.
> 
> Clearly something is wrong, as both programs work the same way. I
> suspect that the compiler doesn't see the connection between
> uselessWord(W) and \+uselessWord(W). It thinks that both could succeed
> or both could fail. In fact when one succeeds, the other fails and
> vice-versa.

This problem is well known and in general it's not solvable (e.g., while
we might expect the compiler to work out that `p' and `not p' are
exclusive and exhaustive, we can't expect it to work out that `p' and
`q' are exclusive and exhaustive, where p and q are arbitrary goals.  A
while back we did have a summer student work on adding support for
`pragma exlusive' and `pragma exlusive_exhaustive' declarations, but
unfortunately that work remains incomplete.

> I just find the latter notation nice and the first one ugly, as in
> predicate logic I would write:
> 
> uselessWord(a)
> uselessWord(her)
> forall W(isu(W,yes) <- uselessWord(W))
> forall W(isu(W,no) <- ~uselessWord(W))
> 
> This looks like the not-compiling example. The compiling one doesn't
> look like logic, as there is no if-then-else in logic. Neither there
> is infix = operation in logic.

Mercury's if-then-else is perfectly logical: ( if A then B else C )
is *semantically* equivalent to ( A, B ; not A, C ); *operationally*
it is implemented more efficiently and is amenable to mode analysis.

> Any chance you could add better determinism detection in mercury so
> that I could use my preferred notation?

As I pointed out in my first paragraph, this isn't a problem you can
solve in general.  We could add support for the special case you cite,
but (a) it crops up far less than you would expect and (b) if-then-elses
are typically clearer to the reader in our experience.  That said, we
are in principle all for improved mode analysis; in practice workable
general solutions are very hard to come by.

Cheers,
-- Ralph
--------------------------------------------------------------------------
mercury-users mailing list
Post messages to:       mercury-users at csse.unimelb.edu.au
Administrative Queries: owner-mercury-users at csse.unimelb.edu.au
Subscriptions:          mercury-users-request at csse.unimelb.edu.au
--------------------------------------------------------------------------