More scasp tests

[sam.neaves]

I am using scasp on swish.

I am trying to understand the denials still…

My code:
https://swish.swi-prolog.org/p/scasp_constraint_tests.pl

% s(CASP) Programming
:- use_module(library(scasp)).

false :- list1_list2(_List1,List2),my_length(List2,4).

p(1).
p(2).
p(3).

my_length([],0).
my_length([_|List],Len):-my_length(List,Len0),Len is Len0+1.

list1_list2(List,[P|List]):- p(P).

list1_list2_h(List1,List2):- list1_list2(List1,List2),my_length(List2,_Len).

/** <examples> Your example queries go here, e.g.

?- ? list1_list2([],List).
?- ? list1_list2([3,4],List).
?- ? list1_list2([a,b,c],List).

?- ? list1_list2_h([],List).
?- ? list1_list2_h([3,4],List).
?- ? list1_list2_h([a,b,c],List).

*/

I expected ?- ? list1_list2([a,b,c],List). or at least ?- ? list1_list2_h([a,b,c],List). to fail (due to the explicit call to my_length/2) but neither do.

Am I misunderstanding something here?

[jan]

@sam.neaves

Am I misunderstanding something here?

I don’t know yet. It looks a bit odd program, but I tend to agree ? list1_list2([a,b,c],List). should fail. The original Ciao version loops, so something weird is going on …

[jan]

Ok. It is getting a bit clearer to me

• ? list1_list2(_List1,List2) creates lists [1|_], [2|_] and [3|_].
• ? my_length([1|_],4). correctly succeeds, but on backtracking it goes into an infinite loop. This is correct: it doesn’t know that increasing lengths will never be 4 again. It is still a computer
• Somehow, the conjunction ? list1_list2(_List1,List2), my_length(List2,4). fails. This must be a bug and the Ciao version correctly succeeds once and again goes into an infinite loop.

As a result of the failure in the current implementation, the global constraint holds and therefore we get this result. The global constraint makes Ciao go into a loop. I think that can be improved as if the body of a global constraint succeeds we can cut.

Note that the global constraint is logically always false and therefore no matter which query you use, if it considers this global constraint it will fail.

Now I must figure out why this conjunction fails Thanks for the report!

[sam.neaves]

ok…

The other one I have tried is with the global constraint:

false :- list1_list2(_List1,List2),member(1,List2).

?- ? list1_list2([a,b],List2).
List2 = [1, a, b];

[sam.neaves]

I think any conjunction fails when asked as a query…

? p(1),p(2).
false

[jan]

I noticed that … That part is fixed (also on public SWISH). Unfortunately that was a simple mistake in the query preparation and doesn’t solve the global constraint problem.

My previous remark on the constraints are wrong though. The “correct” response is a model that includes all lists that do not have a length of 4 (in the original example) or, in the new version, all lists that do not contain a 1. As there are an infinite number of such lists, this query should not terminate. There is indeed a bug

[jan]

I think there is no bug after all I’ve reduced the program to this:

% :- c(L).
:- p(_, List2), my_length(List2,2).

c(List2) :-
    p(_, List2),
    my_length(List2,2).

p(X, [P|X]) :-
    p(P).

p(1).

my_length([], 0).
my_length([_|List], Len) :-
    my_length(List, Len0),
    Len is Len0+1.

Now, ? not c(X). is true with one model, complicated language for "Any list that does not start with a 1.

{ not c([A | {A∉[1]}|B]), not p(A | {A∉[1]}), not p(B,[A | {A∉[1]}|B])
}

And ? p(X,Y).

% Model
{ not p(A | {A∉[1]}), p(1),  p(X,[1|X]),  not p(B,[A | {A∉[1]}|B])
}
% Bindings
Y = [1|X] ? 

Which is consistent (I think; not sure this is all Common Sense ). The model comes with a list that starts with 1. The constraint prohibits lists that start with anything but 1.

I think this is just a simplification of your original program.

[sam.neaves]

hmm.

With your program:

?- ? c([1,2]). Is true. This is not what I expect.

@jan

:- p(_, List2), my_length(List2,2).

I would understand to say no model with list2 of a length of 2 is allowed. So a model could have list2 with length 1 or >3 according to the constraint, but :
c(List2) :- p(_, List2), my_length(List2,2).

Says that it has to be length 2. So I would expect ‘false’. As there can be no model where both of these are true.

[jan]

From Joaquin I got this answer:

Nice example.

The denial :- p(, List2), my_length(List2,2). Means that forall _ and List2 the atoms p(, List2), my_length(List2,2) cannot be simultaneously true.

Since p(,[1,]) holds and my_length([1,_],2) also holds there are no models.

The denial :- c(L) means that forall L the atom c(L) must be false.

Again, since c([1,_]) holds the denial discard any tentative model.

Under s(CASP) using --sasp_forall or —prev_forall flags the evaluation generates the model >obtained under Swi-Prolog — which is incorrect.

I’m still scratching my head about all the negations It gave me some hope I had messed up the option processing. Unfortunately that is not the case

[sam.neaves]

Hey Jan - did you have any more thoughts about this?

It seems to me that the implementation of the denials still do not make sense with what we would expect.

[jan]

I did some search, but fixing it stalled. If I recall well it is related to adding a disequality nested inside a term. The Ciao version gets this right, but for the wrong reason (so it gets other things wrong). I’m afraid this will take some time.

[jan]

There is no disjunctive head, so if you want to express either p or q (exclusive) is true, you get

p.
q.

false :- p, q.

The rule p :- p. is currently not supported. Positive variant calls are silently ignored. You can get warnings about this using --warning for the commandline version. Eventually, tabling should solve that, but SWI-Prolog doesn’t support constraints during tabling yet.

[sam.neaves]

I would expect false. My understanding is the denial is that nothing can be true if p and q are true. p and q are said to be true so everything is false such as r.

[jan]

Yip. You state p and q are true and you state state they can’t both be true, so we have no models. Sorry, I hinted at that. What works is this:

:- abducible p, q.

false :- p, q.

r :- p.
r :- q.

It needs a little policing though. It generates discontiguous warnings and floods the model with stuff that should be hidden.

[sam.neaves]

Would that be:

p.
q.

false :- -p, -q.

r :- p.
r :- q.

[sam.neaves]

This would say you can only have p or q:

:- abducible p, q.

-p :- q.
-q :- p.
false :- -p, -q.

r :- p, q.

and

:- abducible p, q.

false :- not p, not q.

r :- p.
r :- q.

Would be to exclude the top row from the table you posted?

[sam.neaves]

I think abducible p add the following

p :- not not_p.
not_p :- not p.

[sam.neaves]

I am not following what your trying to do here. That program does what I expect.

:- abducible p, q.
Means p and q can either be true or false in a model.

false :- -p, -q.
Means if in a model -p and -q are true fail and do not return a model.

r:-p,q.

Means that in a model with p and q it will also have r.

Which is what we get.

[JasonMorris]

@j4n_bur53

But s(CASP) generates only one model, doesn’t it?

My understanding is that s(CASP) generates multiple minimal models, each of which is capable of supporting the goal. I’m not sure what, if anything, that means for the behaviour you’re looking at. You can see in the results of the SWISH you posted that the model being returned is just the third model in which p and q are both true. In that model, r is true.

If what you want to do is determine whether r is true in all models, I think the way to do that in s(CASP) would be to query ? r and then query ? not r, and if the first returns any models, and the second returns none, then you have your result.

In your swish, ? not r returns two models, as you might expect.