Unification booléenne dans Prolog?

Question

Je lutte déjà depuis longtemps avec le problème suivant. Je veux rendre l'unification habituelle de Prolog plus intelligente.

Fondamentalement, je veux que certaines variables comprennent que par exemple 0 = ~ 1 et 1 = ~ 0. Cela ne fonctionne pas normalement:

?- op(300, fy, ~).
true.

?- X = ~Y, Y = 0.
X = ~0,
Y = 0.

Je sais que CLP (B) peut le faire:

Welcome to SWI-Prolog (threaded, 64 bits, version 8.3.7)

:- use_module(library(clpb)).
true.

?- sat(X=:= ~Y), Y = 0.
X = 1,
Y = 0.

Mais j'ai besoin de quelque chose de plus léger que de charger une bibliothèque CLP (B) complète. Des idées?

Answer 1

Il semble que SWI-Prologs quand / 2 fait le travail. J'utilise l'algorithme Quine à partir d' ici pour évaluer partiellement une expression booléenne. Je peux ensuite définir un prédicat booléen let / 2:

let(X, Y) :-
   eval(Y, H),
   term_variables(H, L),
   ( L== [] -> X = H;
      cond(L, R),
      when(R, let(X, H))).

cond([X], nonvar(X)) :- !.
cond([X,Y|Z], (nonvar(X);T)) :-
   cond([Y|Z], T).

Le prédicat ci-dessus réévaluera l'expression affectée à la variable X chaque fois qu'une variable à l'intérieur de l'expression change. L'expression est associée à la variable X via when / 2. Puisque nous voyons quand / 2 dans le niveau supérieur, nous voyons l'expression associée:

?- let(X, ~Y).
when(nonvar(Y), let(X, ~Y))

?- let(X, Y+Z).
when((nonvar(Y); nonvar(Z)), let(X, Y+Z))

Et nous pouvons également faire notre cas d'utilisation et même plus:

?- let(X, ~Y), Y = 0.
X = 1,
Y = 0.

?- let(X, Y+Z), Y = 0.
Y = 0,
when(nonvar(Z), let(X, Z))

?- let(X, Y+Z), Y = 0, Z = 1.
X = 1,
Y = 0,
Z = 1