Controlling Prolog variable value selection

Inspired by an earlier question I tried to implement something that would enumerate the possibilities for a boolean expression. However, I'm having trouble with variable choice. Here's my intended outcome:

?- eval(X^Y, R).
R = 0^0;
R = 0^1;
R = 1^0;
R = 1^1;
no.

Here's my code:

:- op(200, yfx, ^).

split(V, R) :- var(V), R = 0.
split(V, R) :- var(V), R = 1.
split(X ^ Y, XP ^ YP) :- split(X, XP), split(Y, YP).

This already doesn't do what I want even for this simple case:

?- split(Y, R).
R = 0 ;
R = 1 ;
Y = _G269^_G270,
R = 0^0 ;
Y = _G269^_G270,
R = 0^1 ;
Y = _G269^ (_G275^_G276),
R = 0^ (0^0) ;
Y = _G269^ (_G275^_G276),
R = 0^ (0^1) ;
Y = _G269^ (_G275^ (_G281^_G282)),
R = 0^ (0^ (0^0)) .

So, I can see what the problem is here, which is that on the way through split(Y, YP) Prolog has exhausted the first two clauses, so it winds up in split(X^Y, ...) again, unifying my Y with X'^Y', essentially. I am just not sure what I need to do to close off that path except at the outset where I have the structure ^/2.

I'd also like this to work with nested structures, so I can't just eliminate the recursive processing of the branches.

Edit: without operators

If the op/3 is bothering you, consider this formulation:

eval(and(X,Y), R).
R = and(0,0);
R = and(0,1);
R = and(1,0);
R = and(1,1);
no.

This would be the code in that case:

split(V, R) :- var(V), R = 0.
split(V, R) :- var(V), R = 1.
split(and(X,Y), and(XP,YP)) :- split(X, XP), split(Y, YP).

Bear in mind I'd still like it to work with recursive formulations like and(and(X,Y),and(Y,Z)) etc.

Solution

Main problem: Defaulty representation

The core problem in this case is the defaulty representation you are using to represent Boolean expressions.

By "defaulty" I mean that you cannot clearly distinguish the cases by pattern matching: In your case, a variable V may denote either

one of the propositional constants 0 and 1, or
a compound expression of the form A^B.

Due to this shortcoming, you cannot cleanly express a constraint of the form "the variable X stands only for one of the two propositional constants" within your program.

A way out: Clean representation

A declarative way out is to use a clean representation instead.

For example, suppose we arbitrarily use v/1 to distinguish variables that only denote the propositional constants, then we have:

v(X) to denote the propositional variable X
A^B to denote a compound expression.

Clearly, since the principal functors and arities are different (v/1 vs. (^)/2), we can distinguish the cases by pattern matching alone.

With this new representation, your snippet becomes:

split(v(V), V) :- V = 0.
split(v(V), V) :- V = 1.
split(X^Y, XP ^ YP) :-
        split(X, XP),
        split(Y, YP).

Example query:

?- split(v(X)^v(Y), R).
X = Y, Y = 0,
R = 0^0 ;
X = 0,
Y = 1,
R = 0^1 ;
X = 1,
Y = 0,
R = 1^0 ;
X = Y, Y = 1,
R = 1^1.

Note that this still works in all directions, also in the most general case:

?- split(Expr, R).
Expr = v(0),
R = 0 ;
Expr = v(1),
R = 1 ;
Expr = v(0)^v(0),
R = 0^0 ;
Expr = v(0)^v(1),
R = 0^1 ;
etc.

As a rule of thumb, once you have to use an extra-logical predicate like var/1 in your code, there is little hope to retain its logical purity and monotonicity. Aim for clean representations to preserve these properties.

Sometimes, it is unavoidable to use defaulty representations, for example, because you want to make the input easier for users. In such cases, aim to quickly convert them to clean ones before starting the actual reasoning.