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

[Fergus Henderson]

On 03-Feb-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> 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.

Ah.  The language reference manual says that the transformations
to eliminate double negation "preserve or improve mode-correctness:
they never transform code fragments that would be well-moded into
ones that would be ill-moded".  But in fact this is not correct:
as your example shows, the transformation does not necessarily preserve
mode-correctness for code involving mostly-unique modes.

Still, the problem is not too bad.
A simple work-around is to insert an extra call,
e.g.  to `succeed'

	\+ (succeed, \+ P)

where `succeed' is defined by

	succeed --> [].

That is sufficient to inhibit the fairly simplistic
double-negation elimination transformation described
in the language reference manual that occurs before
mode checking.  And of course after mode checking
and the other static checking phases have completed,
the compiler can go ahead and optimize away the call
to `succeed', so you should not need to pay any efficiency
cost for this work-around.

Unfortunately that work-around also exposes a bug in the current
Mercury implementation, due to essentially the same invalid assumption
as in the aforementioned incorrect statement in the language reference
manual.  After inlining and optimizing away the call to `succeed',
the compiler will go ahead and eliminate the double negation, even
though doing this doesn't preserve mode correctness.  As a result it
will then generate incorrect code.  I'm about to commit a fix for
this bug, so this will be fixed in 0.9.2.  Thanks for the feedback --
if you hadn't mentioned this issue, then I wouldn't have spotted that bug.

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

That should work fine too.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------