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

[Ralph Becket]

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