It seems that Prolog is unable to return some specific answers to a query. I wrote a short simple piece of code in SWI-Prolog in which I tried to check that whether a given binary vector C can be generated by a generator matrix G or not. All calculations are in modulo 2. When I call my main predicate codeword/2 for the binary vector [0,1,1], it returns true, which is a correct answer to the query:
codeword([0,1,1],[[1,1,1],[1,0,0]]).
true.
However, when I call the predicate in the query
codeword([X,Y,Z],[[1,1,1],[1,0,0]]),X+Y+Z =:= 2.
it returns false, which is obviously an incorrect answer, because we do know that [0,1,1] is in fact a codeword. In other words, by the first query, we can see that [0,1,1] is indeed a codeword; But the second query indicates that the code does not contain a codeword of weight 2, which is incorrect.
Is it a normal behavior in Prolog? Can we consider it a bug?
Here is what I wrote:
addbinvecs([A],[B],[C]) :-
(A = B -> C = 0; C = 1).
addbinvecs([H1|T1],[H2|T2],[H3|T3]) :-
(H1 = H2 -> H3 = 0; H3 = 1),
addbinvecs(T1,T2,T3).
%%%
allzero([0]).
allzero([H|T]):-
H = 0,
allzero(T).
%%%
codeword(X,[_|_]) :- allzero(X).
codeword(C,[C|_]).
codeword(C,[_|Gt]):-
codeword(C,Gt).
codeword(C,[Gh|Gt]):-
addbinvecs(C,Gh,C1),
codeword(C1,Gt).
To start with your comment:
I didn't employ cuts.
Oh yes, you did! The if-then-else construct you employed implicitly uses a cut and thereby prunes the search space a bit too much. But how can you see that by yourself?
First, take your query and remove the extra condition:
?- codeword([A,B,C],[[1,1,1],[1,0,0]]).
A = 0, B = 0, C = 0
; A = 1, B = 1, C = 1
; A = 0, B = 0, C = 0
; A = 1, B = 0, C = 0
; A = 1, B = 1, C = 1
; false, unexpected, incomplete.
So while these answers are all fine, a further answer is missing. A simple way to fix this is to replace this if-then-else construct by a pure version of it, called if_/3:
:- use_module(library(reif)).
addbinvecs([A],[B],[C]) :-
if_(A = B, C = 0, C = 1).
% (A = B -> C = 0; C = 1).
addbinvecs([H1|T1],[H2|T2],[H3|T3]) :-
if_(H1 = H2, H3 = 0, H3 = 1),
% (H1 = H2 -> H3 = 0; H3 = 1),
addbinvecs(T1,T2,T3).
?- codeword([A,B,C],[[1,1,1],[1,0,0]]).
A = 0, B = 0, C = 0
; A = 1, B = 1, C = 1
; A = 0, B = 0, C = 0
; A = 1, B = 0, C = 0
; A = 1, B = 1, C = 1
; B = 1, C = 1, dif:dif(A,1) % new
; false.
(In SWI, you need to install library(reif), in Scryer and Trealla it is pre-installed.)
This now contains your expected solution, except ... it is a bit too general. It not only admits A = 0, B = 1, C = 1 but also infinitely many other solutions, like
?- codeword([non_binary,1,1],[[1,1,1],[1,0,0]]).
true
; false.
But then, this is what you described in the first place! To narrow it down you would have to state that all variables are binary. That should not be too difficult for you.