eqrel Behavior

[KarlJoad]

I am implementing Datalog for a personal project right now. I have a naive inference engine working. I am starting to scale up my test sizes and came across a behavior in a test that I did not expect. I am double-checking my results for this program against Souffle and Souffle's answers have confused me further. This is broadly a question about the meaning of eqrel in Souffle. My language does not have eqrel right now.

From what I understand, eqrel is an optimization that allows Souffle to more efficiently represent a relation that creates classes of equivalent terms/data. However, since it is an optimization, I expect that I will get the same answer whether or not eqrel is included in a declaration.

Using the following program, I get two different answers, depending on which .decl path I use.

.decl edge(x : number, y : number)
edge(1,2).
edge(2,3).
edge(3,4).

.decl path(x : number, y : number) eqrel
.decl path(x : number, y : number)

path(x,y) :- path(y,x). // Paths are undirected

path(x,y) :- edge(x,y). // A path is an edge

path(x,z) :- edge(x,y), path(y,z).
.output path(IO=stdout)

When I do not have eqrel in the declaration, I get

---------------
path
===============
1	1
1	2
1	3
1	4
2	1
2	2
2	3
2	4
3	1
3	2
3	3
3	4
4	1
4	2
4	3
===============

When I do have eqrel in the declaration:

---------------
path
===============
2	2
2	1
2	3
2	4
1	2
1	1
1	3
1	4
3	2
3	1
3	3
3	4
4	2
4	1
4	3
4	4
===============

The difference between the two is the last path fact found, the 4 4 one. Since eqrel is supposed to be an optimization, how am I getting a different answer with the same program? (My engine behaves like the no-eqrel declaration, but I expected the eqrel declaration's output.)

[quentin]

You can read more about eqrel in https://souffle-lang.github.io/relations#equivalence-relations and the paper https://souffle-lang.github.io/pdf/pact2019eqrel.pdf

It is an optimization in the sense that you don't have to write explicit reflexivity, symmetry and transitivity rules and it will perform better than if you had.

In your exemple, path has a symmetry rule but no reflexivity or transitivity rule, so you cannot expect to get the same output when eqrel add them for you.

Maybe you want to add a reflexivity rule and change path(x,z) :- edge(x,y), path(y,z). into a transitivity rule: path(x,z) :- path(x,y), path(y,z)., in that case you get the same result as eqrel.

To summarize:

.decl edge(x : number, y : number)
edge(1,2).
edge(2,3).
edge(3,4).

path(x,y) :- edge(x,y). // A path is an edge
.output path(IO=stdout)


//--- either these five lines
.decl path(x : number, y : number)
path(x,y) :- path(y,x).            // symmetry
path(x,x) :- path(x,_).            // reflexivity
path(x,x) :- path(_,x).            // reflexivity (not really needed since subsumed by symmetry rule)
path(x,z) :- path(x,y), path(y,z). // transitivity

//--- or just this line
.decl path(x : number, y : number) eqrel

[KarlJoad]

Ah, yes! I found the definition of Souffle's eqrel and thoroughly read it after I opened this question. Adding the transitivity rule was what solved it for me (in both Souffle and my engine). It makes sense that there is no path 4 -> 4 without the transitivity, because there is no rule that could unify the 4->3 and 3->4 facts into 4->4. Reading the PACT paper is on my TODO list for the near future. I want to implement eqrel or something similar in my Datalog implementation, but I have bigger optimization fish to fry first.

I'm not sure how I managed to get the eqrel answer without reflexivity in this example, but that might be something else.

I copied (and "translated" for my language) this particular path reachability definition from online, so I guess this is what I get for blindly copying code from the Internet without reading and/or understanding it (although the page seems like an idea dump page, so using that may not have been the right move).