[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

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
			X1 = X0     % Have to rename since this
		)                 % is in a negated context and
	  then                  % cannot export any results.
		X = X0

which is the same as

verify(P, X0, X) :-
	( if
		( if some [X1] P(X0, X1) then fail else true )
		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


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

which is what we wanted.

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

More information about the users mailing list