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.

回答1:

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.

回答2:

At some point of time I wrote a very small program that seems to be more or less what you are looking for. I really hope I am not totally misreading your question. You can check this SWISH program for the whole program. There are a few differences, like using f and t instead of 0 and 1, or using and and or instead of ^ and v. However, the basic idea is the same as yours (I think).

If I remove some of the unnecessary stuff for demonstrating, then this would be the program:

:- op(100, fy, ?).
:- op(500, yfx, and).
:- op(500, yfx, or).

table(F, T) :-
        term_variables(F, Vs),
        bagof(R-Vs, bl(F, R), T).

bl(?X, R) :-
        v(X, R).
bl(X and Y, R) :-
        bl(X, R0),
        and_bl(R0, Y, R).
bl(X or Y, R) :-
        bl(X, R0),
        or_bl(R0, Y, R).

v(f, f).
v(t, t).

and_bl(f, _, f).
and_bl(t, Y, R) :- bl(Y, R).

or_bl(f, Y, R) :- bl(Y, R).
or_bl(t, _, t).

The main point here is that I have a pure relation, my v/2, which simply states that the value of true is true and the value of false is false. Then, I am using a mutually recursive definition for actually evaluating the boolean expressions, which eventually bottoms out at v/2.

I decided to "tag" the boolean variables myself, so instead of X you would have to write ?X. If I remember correctly, at the time I realized I need a way to explicitly say if I have a Boolean variable within an expression, or if the whole expression is still "unknown". In other words, this: ?X is either t or f and this: Expr can be ?X, or not ?X, or ?X and ?Y, or ?X or ?Y, or not (?X and ?Y), and so on.

Tagging the variable with ?X is what avoids the "defaulty representation" is what @mat explained. Importantly, without explicitly tagging, I don't see a way for telling apart Boolean variables from Boolean expressions.

Here is how you can use it:

?- bl(?t and ?X, R).
X = R, R = f ;
X = R, R = t.

?- bl(?t or ?X, R).
R = t.

?- bl(?A or (?B and ?C), R).
A = B, B = R, R = f ;
A = C, C = R, R = f,
B = t ;
A = f,
B = C, C = R, R = t ;
A = R, R = t.

?- table(?A or (?B and ?A), R).
R = [f-[f, f], f-[f, t], t-[t, _7734]].

回答3:

There are already two good answers, a pure one and the shorter one using term_variables/2. I would still like to address a detail:

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.

If you don't want to perform the head unification with X^Y if the first argument is a variable, pull the unification out of the head. Nothing forces you to put the term X^Y there! What you want to do is to only consider your last clause if the previous two clauses did not apply. The previous two clauses were guarded by var/1, so you can guard the last one with nonvar/1:

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

With this your examples work as intended:

?- split(Y, R).
R = 0 ;
R = 1 ;
false.

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

Edit: As mat pointed out in the comments, using tests like var/1 can get you into all kinds of trouble.

One problem is that there are various levels of instantiation that you would have to check carefully: mat's example query of split(1, R) fails with the above code (it should succeed with R = 1). This is because 1 falls into the nonvar case but does not unify with _^_. If we're going this way, we must distinguish not just the var and nonvar cases, but rather var, ground, and nonvar-but-not-ground. This gets a bit messy.

Another issue is the query split(V, R), V = 1, which is declaratively equivalent to the query above, but succeeds twice, including with the solution R = V. This is because this definition of split/2 (deliberately) avoided introducing sharing between its arguments. Whether we do want that sharing or not depends on the specification.

I won't try to give a fully robust solution with instantiation tests as my point was not that this is the best way to go.