[mercury-users] Verify, double negation and if-then-else

Ralph Becket rbeck at microsoft.com
Thu Feb 3 23:11:44 AEDT 2000

In Prolog one would use the idiom `\+ \+ P' to verify
that P could succeed, but without unifying any variables.

In Mercury, however, `not not P' is simplified to just
`P', but this isn't normally a problem because, thanks
to the mode system, P is going to be idempotent (this
isn't necessarily the case with Prolog).

There is a situation, though, where this doesn't work.
The problem arises with the use of mostly unique
structures.  The reason I'm posting this is that one
has to take care over quantification to see that it
works.

If I have `P(mdi, muo) is semidet', I would like some
way of verifying whether P will succeed without changing
the mostly unique argument.  As I've just mentioned, the
double negation idiom won't do the trick.  So the next
thing to try is

% dcg_not//1 is needed because of a current bug.
dcg_not(P) --> ( if P then { fail } else [] ).

verify(P) --> dcg_not(dcg_not(P)).

This expands to

verify(P, X0, X) :-
some [X1]
( if
( if P(X0, X1) then
fail
else
X1 = X0     % Have to rename since this
)                 % is in a negated context and
then                  % cannot export any results.
fail
else
X = X0
).

which is the same as

verify(P, X0, X) :-
( if
( if some [X1] P(X0, X1) then fail else true )
then
fail
else
X = X0
).

Now, If I write A <=> P(X0, X), B <=> some [X1] P(X0, X1)
and C <=> X = X0 then verify/3 is formally equivalent to

(D, fail) ; (not D, C)
<=> (not D, C)

where D <=> (B, fail) ; (not B, true)
<=> not B

giving

(not D, C)
<=> (not (not B), C)
<=> (B, C)
<=> ((some [X1] P(X0, X1)), X = X0)

which is what we wanted.

Ralph
--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au