Unexpected result of ge on -0.0 and 0.0 under magic rewrite

[DerZc]

Hi,

Consider the following program:

phve[a, b] <- [[-0.0, null], [0.0, null]]
xukw[A, B] := phve[A, B], ge(A, 0)
nwku[F] := phve[_, F]

ssie[C, F] := nwku[C], xukw[F, C]
?[a, b] := ssie[a, b]

I get the results [[null, -0.0], [null, 0.0]], but the value of nwku is [[null]] and the value of xukw is [[0.0, null]], so the result of ssie should not be [null, -0.0].

I also tried to add :disable_magic_rewrite true, then I got correct results.

I can reproduce this on version 0.7.1

[zh217]

Interesting, seems that this only happens with -0.0 and not with any other number.

[zh217]

The gist of the problem can be summarized in:

?[] <- [[0.0 >= 0, -0.0 >= 0, -0.0 >= 0.0, 0.0 >= -0.0]]

The result is true, true, false, true in CozoDB. It looks like the second one shouldn't be true, but actually, for python, it is:

>>> 0.0 >= 0
True
>>> -0.0 >= 0
True
>>> -0.0 >= 0.0
True
>>> 0.0 >= -0.0
True

Not sure what can be done. Going the python way basically means that we will eliminate -0.0 from numbers, and I'm not sure that's what we want to do. Making the second one false as well means that we could mess up with the memcomparable format. Floating point numbers are hard.

At least throwing away -0.0 is self-consistent. So if everything else fails, maybe we will go the Python way.

[zh217]

It seems Rust agrees with python:

assert!(0.0 >= -0.0);
assert!(-0.0 >= 0.0);

passes.

[DerZc]

Hi @zh217 I have a small question. For this test case, is this problem caused by the transformation of ge(A, 0) to ge(A, 0.0) under the magic rewrite?

[zh217]

No, magic rewrite doesn't change that. It is caused by magic rewrite enabling range scan on the relation phve instead of testing every value. Range scan uses the byte order of memcomparable, which in this case differs from the usual comparison in subtle ways.

[DerZc]

I got it! Thank you very much!

[DerZc]

I'm very sorry to disturb you. But I have another question. When does the magic set rewrite get triggered?
The following program should be equivalent to the this test case:

phve[a, b] <- [[-0.0, null], [0.0, null]]
xukw[A, B] := phve[A, B], ge(A, 0)
ssie[C, F] := phve[_, C], xukw[F, C]
?[a, b] := ssie[a, b]

But this program produces correct results, which means it not triggers range scan.

(By the way, there is a small error in the document of magic set rewrite https://docs.cozodb.org/en/latest/execution.html#magic-set-rewrites, the first line of the example should be reachable[a, b] := link[a, b], otherwise, b is unbound.)

[DerZc]

Hi @zh217 so sorry to disturb you. Do you have documents available that outlines the specific case under which the magic set rewrite is applied? I just have the questions mentioned above.

[zh217]

Sorry I haven't had time to look at the above behaviour yet. Magic set rewriting is a standard optimization technique for optimizing Datalog programs, and there are quite a few review articles describing it in details, the one easiest to read is probably Datalog and Recursive Query Processing. Our implementation follows their descriptions. Note that the rewriting technique only applies to pure Datalog, that is, without negation, aggregation, etc., so any time any of these are encountered they are left as it is. Once you know the terminologies of magic set rewriting, the result of ::explain {<query>} should make more sense.

[DerZc]

I got it! Thank you very much for taking the time to respond to me amid your busy schedule!