Re: [eclipse-clp-users] Problem with double delayed negation

Stephan Schiffel wrote:
> Dear all,
> 
> I stumbled across a problem using delayed negation (~/1, ~=/2).
> The following small program demonstrates my problem:
> 
> %%
> p(_X) :- A~=1, A=1.
> p1 :- ~ p(1).
> p2 :- ~ p(X), X=1.
> %%
> 
> ?- p1. succeeds as it should, but
> ?- p2. fails despite being equivalent to p1
> 
> Is this a bug? If not, is there any way to make p2 work as expected?

Negation of general goals has always been a tricky issue in
Logic Programming...  The ~/1 predicate is a rather old part
of ECLiPSe and is defined basically as

delay ~(Goal) if nonground(Goal).
~(Goal) :- call(Goal), !, fail.
~(_Goal).

A later addition to ECLiPSe was the priority system for delayed
goals: this "stratifies" the execution such that only higher
priority goals can interrupt lower priority ones.  This is good
for constraints, but you see in your example that it does not
play too well with ~/2, which can call arbitrary subgoals.

What happens is that ~p(1) wakes up (with priority 2) and calls
p(1), still under priority 2.  Unfortunately, this prevents the
delayed subgoal of p(1), the 1~=1, from executing because it
doesn't have a high enough priority.  Therefore p(1) succeeds,
and ~p(1) wrongly fails.

It looks to me like ~/1 needs some serious thinking if we want
to make it safe and useful for this kind of scenario.  But to solve
your immediate problem: if you know that your negated goal only
contains constraints/delayed goals with a certain minimum priority,
then you can make it work by adjusting the priority of ~/1 to be
lower (higher number) than that priority.

:- set_flag((~)/1, priority, 9).  % anything higher than 2

This makes your p2 succeed (but would not fix the case of nested
~/1, as in your bug report from yesterday).


-- Joachim