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

From: Stephan Schiffel <stephan.schiffel_at_googlemail.com>
Date: Fri, 9 Dec 2011 10:40:14 +0000
Joachim Schimpf wrote:
> 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
> 
> 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.

Thanks for the explanation.

So to make it work, I'd need to make the priority of each nested ~/1 one 
higher than the one surrounding it? E.g., by doing something like this:

p(_X) :- lazy_neg(A=1), A=1.
p1 :- lazy_neg(p(1)).
p2 :- lazy_neg(p(X)), X=1. 

lazy_neg(Goal) :-
	get_priority(Prio),
	Prio1 is Prio-1,
	lazy_neg(Goal, Prio1).

lazy_neg(Goal, Prio) :-
	( nonground(Goal, Var) ->
		suspend(lazy_neg(Goal), Prio, Var->inst)
	;
		\+ Goal
	).

However, this is not a general solution because there are only 12 priorities. 

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

Unfortunately, this is generated code and there is no upper bound on the 
number of nested negations that are in there. So I guess, I'll have to do it 
without delayed negation.

Maybe it would be a good idea to have a remark in the documentation warning 
about the use of nested delayed negations.

Cheers,
Stephan
Received on Fri Dec 09 2011 - 10:40:26 CET

This archive was generated by hypermail 2.2.0 : Thu Feb 02 2012 - 02:31:58 CET