2

I am struggling alreay for a long time with the following problem. I want to make the usual unification of Prolog more smart.

Basically I want that certain variables understand that for example 0 = ~1 and 1 = ~0. This doesn't work normally:

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

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

I know that that CLP(B) can do it:

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.

But I require something more lightweight than loading a full CLP(B) library. Any ideas?

  • Unification is syntactic . You are hoping to achieve a semantic interpretation whereby reasoning is done over semantic value obtained from the syntactic representation . – Kintalken Nov 14 '20 at 15:56
  • Yes You can and should do that but what You call `my_unification` is not unification anymore , a better name would be `my_evaluation` , – Kintalken Nov 15 '20 at 02:28
  • Would it not be best if unification was reserved to mean syntactic unification ? – Kintalken Nov 15 '20 at 20:20
  • These is nothing wrong talking about E-unification where E is some equational theory. See also: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#E-unification , here E = Boolean algebra/ring . –  Nov 15 '20 at 21:18

1 Answers1

0

It seems that SWI-Prologs when/2 does the job. I am using the Quine algorithm from here to partially evaluate a boolean expression. I can then define a Boolean let/2 predicate:

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).

The above predicate will reevaluate the expression assigned to the variable X when ever some variable inside the expression changes. The expression is associate with the variable X through when/2. Since we see when/2 in the top-level, we see the associated expression:

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

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

And we can also do our use case and even more:

?- 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