my code on swish looks like this:
% s(CASP) Programming
:- use_module(library(scasp)).
%:- style_check(-discontiguous).
:- style_check(-singleton).
%:- set_prolog_flag(scasp_unknown, fail).
% Your program goes here
% sCASP encoding of rps
% Reference: Jason's article at https://medium.com/computational-law-diary/how-rules-as-code-makes-laws-better-115ab62ab6c4
#pred player(X) :: '@(X) is a player'.
#pred participate_in(Game,Player) :: '@(Player) participated in @(Game)'.
#pred winner(Game,Player) :: '@(Player) is the winner of @(Game)'.
#pred throw(Player,Sign) :: '@(Player) threw @(Sign)'.
#pred beat(Sign,OtherSign) :: '@(Sign) beats @(OtherSign)'.
#pred game(G) :: '@(G) is a game of rock-paper-scissors'.
beat(rock,scissors).
beat(scissors,paper).
beat(paper,rock).
winner(Game,Player) :-
game(Game),
player(Player),
player(OtherPlayer),
Player \= OtherPlayer,
participate_in(Game,Player),
throw(Player,Sign),
participate_in(Game,OtherPlayer),
throw(OtherPlayer,OtherSign),
beat(Sign,OtherSign).
% There is a Game in which Bob and Jane played.
game(testgame).
player(bob).
player(jane).
participate_in(testgame,bob).
participate_in(testgame,jane).
throw(bob,rock).
throw(jane,scissors).
/** <examples> Your example queries go here, e.g.
?- ? winner(testgame,Who).
*/
If I run the query ?- ? not winner(testgame, bob).
, I get the expected result, which is no models. If you modify the code to make the disequality the last line of the winner
rule, it returns one incorrect model.
I tried the same code in the Ciao implementation of s(CASP) and got essentially identical results, so it doesn’t seem like an issue with the port. If anything, SWISH produced the incorrect result must more efficiently.
Here’s the model SWISH gives:
? not winner(testgame,bob).
s(CASP) model
testgame is a game of rock-paper-scissors
there is no evidence that A not bob, or jane is a player
bob is a player
jane is a player
there is no evidence that rock beats rock
bob participated in testgame
there is no evidence that bob threw B other than rock
there is no evidence that bob threw C other than rock
there is no evidence that bob threw D other than rock
bob threw rock
there is no evidence that bob is the winner of testgame
The dual program generated by Ciao scasp when you run scasp --code rps.pl
includes, as the next-to-last definition of the predicate, when the disequality is last in the clauses:
not o_winner_1(Var0,Var1,Var2,Var3,Var4) :-
game(Var0),
player(Var1),
player(Var2),
participate_in(Var0,Var1),
throw(Var1,Var3),
participate_in(Var0,Var2),
throw(Var2,Var4),
not beat(Var3,Var4).
I think this is the version of the rule that is getting triggered, because it is the only one with not beat
included, and not beat(rock,rock)
is in the resulting model.
It’s incorrect because it is excluding the one remaining condition, the disequality. If you haven’t considered whether or not the two players are allowed to be the same player, then the fact that the player doesn’t beat themselves doesn’t mean the person didn’t win.
I think the problem is the way the duals are constructed. not o_winner_1/5
is defined several times, each time adding just one of the original clauses, negated. In every subsequent definition, anything added previously is kept, but no longer negated.
So if the original rule is:
1 :- 2, 3, 4.
you get
not 1 :- not 2.
not 1 :- 2, not 3.
not 1 :- 2, 3, not 4.
It seems to me that it would be more correct if we got something like this:
not 1 :- not 2, 3, 4.
not 1 :- 2, not 3, 4.
not 1 :- 2, 3, not 4.
not 1 :- not 2, not 3, 4.
not 1 :- 2, not 3, not 4.
not 1 :- not 2, not 3, not 4.
Let me know if I’m out to lunch. Fighting with s(CASP) to make duals work properly was my least favourite part of dealing with it last year. Would be great to improve on that.
This excellent example of the problem was brought to my attention by Eric at this medium reply.