Analysis of divergence from Euler.js

[sto0pkid]

The discovery of this divergence was one of the big roadblocks we ran into. I've recovered the following insights from old chat logs, but have not recently reproduced any of these experiments or reviewed these pieces of each codebase in enough detail to be currently confident in the accuracy of the statements:

There were apparently a couple different places of divergences:

1. Unification method in ep check

   • univar: ep-check checked if terms were equivalent, i.e. vars can only match with other vars and constants can only match with identical constants, lists can only match with equivalent lists, ... this is why we have a special unify_ep function
   • euler.js: ep-check just checked if the terms unified

2. Ep-check timing

   • univar: ep-check for a call to rule A is always just checking previous calls to A
   • euler.js: ep-check for a call to rule A is checking previous calls to B, where B is the rule calling A I apparently reached a conclusion on this one, "the relation between euler.js & univar wrt [this difference]... euler.js is ultimately cutting the same rules that we're cutting. it just does it in a weird way. instead of just not running the rule, it runs the rule but doesn't let any of its body items do anything. so as far as results go, this is just a slow way of just not running the rule, i.e. like "

3. Search strategy

   • univar: DFS
   • euler.js: BFS The conclusion I reached on this one was that the method shouldn't matter on a finite / non-looping search space as far as result-set semantics.

4. "f != false" vs. "f != null" bug

   • just a regular bug in euler.js, not a point of semantic confusion, just pointing it out for awareness

The following example should apparently demonstrate the difference in result-set semantics between the method we followed with univar and the method followed by euler.js:

kb
A :p B. B :p C. C :p D.
D :p C. C :p B. B :p A.
{?z :p ?y. ?y :p ?x} => {?x :p ?z}.
fin.
query
?what :p A.
fin.

should include

D p A
B p A
C p A
A p A

while Euler only gets

B p A
C p A
A p A

The example was apparently crafted with the constraints: "so we need an example where every search-path that leads to some result requires at least 2 recursive calls of a rule, and for some n > 1, it fails the ep-check on the nth recursive call along that search-path, and ofc it must be ep-checks that univar wouldnt fail"

My conclusion was that the divergence in result-sets was entirely due to the difference in unification method used in the ep-check, and that the other differences did not have any effect on result-sets.

The example when run with a modified euler.js that corrected the unification method found all 4 results, but took 16 million steps to finish, taking hours to run, crashing browsers, etc... It ran for so long that the default assumption was that it was an infinite loop and the alternative algorithm must have been wrong. But then it did terminate, with all the expected results, whereas euler.js failed to find a result that it seemed like it should have "obviously" gotten. "dmiles: thats totally nut that eye/jos/euler is only giving three answers"

We never really reached a conclusion about what to do about this situation. The purpose of this issue is to reunderstand this whole situation and make a determination about where to go from here.

[sto0pkid]

EYE produces all expected results

[sto0pkid]

In the EulerJS repo,

• https://github.com/sto0pkid/EulerJS/blob/main/eulerjs/versions/euler_js_ep_fixed_1.js demonstrates the "Ep-check timing" difference
• https://github.com/sto0pkid/EulerJS/blob/main/eulerjs/versions/euler_js_ep_fixed_2.js demonstrates the "Ep -check timing" + "Unification method in ep check" differences
• https://github.com/sto0pkid/EulerJS/blob/main/eulerjs/versions/euler_js_false_fixed.js demonstrates the "f != false vs. f != null" bug

[sto0pkid]

Failed test is here: https://github.com/sto0pkid/EulerJS/blob/main/eulerjs/examples/failed_test.js

It is the same one we mentioned in the chat logs, and it fails in the expected way. In the chat logs it was mentioned that EYE also failed on the same test but I don't currently have that version of EYE to test. In any case, this may be a positive since it demonstrates that the euler.js algorithm was wrong, as we expected, and that there's some "simple" fix in EYE which also doesn't produce the complexity explosion.