E-Graph matching with monotonic tabling

General
1

Hello,
I have recently stumbled at a very interesting data structure called e-graph (equivalence graph) used to implement term rewriting system (TRS).
When we try to do TRS in prolog, although the formulation is quite elegant, we are immediately confronted to the explosion of possible rewrites.
E-Graph kind of avoid this explosion by grouping equivalent nodes in classes and apply rewrites on classes.
Here is a nice blog post explaining egraph in general, and another that implements it in chr.

I already have tested multiple approach and currently trying to reuse monotonic tabling for applying rewrite rules.
Here is a minimal implementation of the idea with commutative and associative rewrite rules for addition:

:- table (match/2, rewrite/2, rule/2) as monotonic.
:- dynamic node/2 as monotonic.

% flattened representation of (a+b)+c
% node(Node, Class)
node(a, a).
node(b, b).
node(c, c).
node(a+b, ab).
node(ab+c, abc).

% commutativity
rule(A+B, B+A).
% associativity
rule(AB+C, A+BC) :-
   node(A+B, AB),
   % don't insert BC if it already exists
   (  node(B+C, BC)
   -> true
   ;  node(B, BClass),
      node(C, CClass),
      atom_concat(BClass, CClass, BC),
      assert(node(B+C, BC))
   ).

rewrite(X, X).
rewrite(X, Z) :-
   rule(X, Y),
   rewrite(Y, Z).

match(Y, Class) :-
   node(X, Class),
   rewrite(X, Y).

:- prolog_listen(match/2, connection_change).

connection_change(Type, _:match(From, To)) :-
   format('~p: ~p are now match~n', [Type, From-To]).

This already works quite well:

?- match(_Node, _Class), Node = _Node-_Class.
new_answer: c+a-ca are now match
new_answer: a+c-ca are now match
new_answer: c+b-bc are now match
new_answer: b+c-bc are now match
Node = c-c ;
Node = b-b ;
Node = a-a ;
Node = c+b-bc ;
Node = c+a-ca ;
Node = c+ab-abc ;
Node = b+c-bc ;
Node = b+a-ab ;
Node = a+c-ca ;
Node = a+b-ab ;
Node = ab+c-abc.

But it is missing 4 nodes: [a+bc, bc+a, b+ac, ac+b].
Very weirdly, querying [a+bc, bc+a] directly works ???

?- match(a+bc, abc).
true.

?- match(bc+a, abc).
true.

But not [b+ac, ac+b]:

?- match(ac+b, abc).
false.

?- match(b+ac, abc).
false.

I am kind of stumped, could somebody explain why ?

2 Likes
2

Ah, my bad, it was the construction of the BC class name in the assoc rule which was incorrect:

rule(AB+C, A+BC, assoc) :-
   node(A+B, AB),
   (  node(B+C, BC)
   -> true
   ;  node(B, BClass),
      node(C, CClass),
      % need to sort subclasses so that the resulting class is unique with respect to permutation
      sort([BClass, CClass], [C1, C2]),
      atom_concat(C1, C2, BC),
      assert(node(B+C, BC))
   ).

Now it works:

?- match(_Node, _Class), Node = _Node-_Class.
new_answer: c+a-ac are now match
new_answer: a+c-ac are now match
new_answer: c+b-bc are now match
new_answer: b+c-bc are now match
Node = c-c ;
Node = b-b ;
Node = a-a ;
Node = bc+a-abc ;
Node = c+b-bc ;
Node = c+a-ac ;
Node = c+ab-abc ;
Node = ab+c-abc ;
Node = ac+b-abc ;
Node = b+c-bc ;
Node = b+ac-abc ;
Node = b+a-ab ;
Node = a+c-ac ;
Node = a+b-ab ;
Node = a+bc-abc.
2 Likes
3

Unfortunately, it seems that the implementation is not completely correct.
I get 195 nodes for 5 additions, whereas I should get 185 nodes…

node(a, a).
node(b, b).
node(c, c).
node(d, d).
node(e, e).
node(a+b, ab).
node(ab+c, abc).
node(abc+d, abcd).
node(abcd+e, abcde).

% use a global counter to generate class ids
next(Next) :-
   nb_getval(next, Next),
   Next1 is Next + 1,
   nb_setval(next, Next1).

:- nb_setval(next, 1).

rule(AB+C, A+BC, assoc) :-
   node(A+B, AB),
   (  node(B+C, BC)
   -> true
   ;  next(BC),
      assert(node(B+C, BC))
   ).

?- time(once(match(_, _))), findall(Node-Class, match(Node, Class), Nodes),
   length(Nodes, N).
Nodes = [3+e-20, 3+b-7, 3+b-32, 3+a-29, 3+a-8, 3+ab-abcd, 2+b-abc, ... + ... - 7, ... - ...|...],
N = 195.

I am wondering if this is because I haven’t written the full congruence closure ?
Anybody has an idea ?