New egraph pack v0.1.0 annoucement for term rewriting

General
1

Hello all,

I have finally managed to publish the first version of my egraph (Equivalence Graph) implementation in swi-prolog !
For a bit of context, I have already made an earlier post detailing how I implemented the egraph.

I’m going to make a very big claim here that this pack provides the fastest term rewriting system implementation of the prolog world !
The reason for me to say this is that this implementation can do full equality saturation of a 10 additions term with commutativity and associativity rewrite rules in under 15 sec (on my laptop).
For comparison, this blog post says that egglogg (a popular rust implementation of egraph) can do this in under a second, while his chr implementation can’t do even a 7 addition term.
If anyone knows of a prolog TRS that can do this faster, please tell us :slight_smile:

What’s new is that I have finally managed to implement a rule compiler to translate rewrite rules into efficient compiled predicates.
Here is an example from the readme:

% myrule.pl
:- use_module(library(egraph)).

% Algebraic rules
egraph:rewrite(comm_add, A+B, B+A).
egraph:rewrite(assoc_add, A+(B+C), (A+B)+C).

% Rules with custom cost
egraph:rewrite(factorize_aa, A+A, 2*A, [cost(9r10)]).

% Rules with left-hand side conditions
egraph:rewrite(reduce_add0, A+B, [const(B, 0)], A, []).

% Rules with a Prolog body
egraph:rewrite(constant_folding, A+B, [const(A, VA), const(B, VB)], VC, [const(VC)]) :-
   VC is VA + VB.

Then you can use it like this:

?- use_module(library(egraph)).
true.

?- phrase((
       % convert a prolog term into an e-graph,
       % Optimized will be the rewritten term
       add_term(a+0, Optimized),
       saturate([reduce_add0]), % apply rewriting rules
       extract % extract optimal cost term in Optimized
   ), [], _Graph).
Optimized = a,
...

The rule compiler has the following features:

  • use prolog terms to match and rewrite terms
    • use '$VAR(Var)` to match literal prolog var
  • the rewritten term can have a custom cost, so that extraction will prioritize lower cost nodes
    the default cost is linked to the size of the prolog term (atomic cost is 1, compound is arity + 1)
  • you can match and attach const number property nodes. this is how the constant folding rule is implemented, as well as add arbitrary prolog code in the body of the rule.

To install, you can just do:

$ swipl pack install egraph

You’ll just need swi-prolog > 9.3.23 because the pack uses ==> SSU DCG rules.

Please, report any feedback, bugs or thought here or in the github issue page.
I know that TRS are used in popular clp packages like clpBNR (@ridgeworks) and clpfd.
I would really like to have opinion of the author of those packages if this could be useful to them ?

1 Like