Logical equivalence in Prolog

Question

I got two expressions to list all lists of bits using Prolog:

bit(0).
bit(1).

bitlist1([]).
bitlist1([B|Bs]) :-
    bit(B),
    bitlist1(Bs).

bitlist2([]).
bitlist2([B|Bs]) :-
    bitlist2(Bs),
    bit(B).

I can't quite see if they are logically equivalent and even if they both really list ALL bit lists.

As I'm using SWI-Prolog I got the following outputs:

?- bitlist1(Bs).
Bs = [] ;
Bs = [0] ;
Bs = [0, 0] ;
Bs = [0, 0, 0] ;
Bs = [0, 0, 0, 0] ;
Bs = [0, 0, 0, 0, 0] ;
Bs = [0, 0, 0, 0, 0, 0] ;
Bs = [0, 0, 0, 0, 0, 0, 0] ;
Bs = [0, 0, 0, 0, 0, 0, 0, 0] ;
Bs = [0, 0, 0, 0, 0, 0, 0, 0, 0] ;
Bs = [0, 0, 0, 0, 0, 0, 0, 0, 0|...] ;
...

?- bitlist2(Bs).
Bs = [] ;
Bs = [0] ;
Bs = [1] ;
Bs = [0, 0] ;
Bs = [1, 0] ;
Bs = [0, 1] ;
Bs = [1, 1] ;
Bs = [0, 0, 0] ;
Bs = [1, 0, 0] ;
Bs = [0, 1, 0] ;
Bs = [1, 1, 0] ;
Bs = [0, 0, 1] ;
Bs = [1, 0, 1] ;
Bs = [0, 1, 1] ;
Bs = [1, 1, 1] ;
Bs = [0, 0, 0, 0] ;
...

bitlist1 starts listing all bit lists containing only zeros and starts listing all others afterwards but this actually can't be seen as Prolog lists an endless stream of bit lists containing only zeros.

bitlist2 lists all combinations of 0 and 1 of every length and afterwards continues with the bit lists with the length higher length.

So they are logically equivalent imo, only the output order of the bit lists differ.

Maybe anyone can confirm my guess or explain why the two expressions aren't logically equivalent? Would be great.

Answer 1

Citing Vannoord

The problem whether two expressions are logically equivalent is undecidable for any `interesting' logic.

Then, because of incompleteness of Prolog search, you should somewhat restrict your proof criteria. I would state the equivalence arise from the fact that

for any given N, it's not possible to find a length(L, N), bitlist1(L), bitlist2(L) that fail. Indeed

2 ?- length(L,N), bitlist1(L), bitlist2(L).
L = [],
N = 0 ;
L = [0],
N = 1 ;
L = [1],
N = 1 ;
L = [0, 0],
N = 2 ;
L = [0, 1],
N = 2 ;
L = [1, 0],
N = 2 ;
L = [1, 1],
...

Answer 2

On a logical level, both predicates are equivalent, since "," in a rule is interpreted as logical conjunction which is commutative(the easiest way to check this is by looking at the truth tables for A & B -> C and B & A -> C, but also sequent calculus or some other proof calculus does the job).

For pure prolog programs, the set of answers of logically equivalent predicates is the same. Since prolog uses depth first search as a search strategy, one predictae might not terminate in case the others do:

?- bitlist1([a|Xs]).
false.

?- bitlist2([a|Xs]).
^CAction (h for help) ? abort
% Execution Aborted

The reason is that prolog tries to prove the goals one after each other. In the case of bitlist1, the first goal is bit(B) where prolog can immediatly decide that bit(a) does not hold. In the case of bitlist2, prolog first tries to prove bitlist2(Bs) and recursively does this for the tail of the Bs list which leads to an infinite recursion. So even if both predicates are logically equivalent, they behave differently.

For your problem of looking at the solutions, you could try to enumerate the lists in increasing length:

?- length(X,_), bitlist1(X).
X = [] ;
X = [0] ;
X = [1] ;
X = [0, 0] ;
X = [0, 1] ;
X = [1, 0] ;
X = [1, 1] ;
X = [0, 0, 0] ;
X = [0, 0, 1] ;
X = [0, 1, 0] .

?- length(X,_), bitlist2(X).
X = [] ;
X = [0] ;
X = [1] ;
X = [0, 0] ;
X = [1, 0] ;
X = [0, 1] ;
X = [1, 1] ;
X = [0, 0, 0] ;
X = [1, 0, 0] ;
X = [0, 1, 0] .

the length predicate gives the relation between a list and its length. We now rely on the fact that length(X,_) produces lists of free variables of increasing length. Then the goal bitlist(1/2) will be called on a fixed size list and prolog will find all solutions for that size before backtracking and trying the next larger list.

Please note that this trick only reorders solutions, but does not change termination in general:

?- X=[a|Xs], length(X,_), bitlist2(X).
^CAction (h for help) ? abort
% Execution Aborted

This still fails because prolog needs to check all lists X not to start with a, but the check is only done after the recursive goal.

Answer 3

In pure logic, order of operations is irrelevant, since everything is an idempotent function. So as long as you have no cuts or side effects, A, B and B, A are equivalent.

Answer 4

I'm not sure you should be discussing pure logical meaning of a predicate and then demonstrating it with an actual Prolog program.

Your first predicate, for example, will actually never run out of 0. There is no "afterwords", or the "afterwords in the search tree is surely never going to be visited. This is of course if you use it for generating answers; using it for validating does not exhibit this behaviour.