Inconsistent results of two equivalent programs

[DerZc]

Hi,

Consider the following program:

kayy[a, b] <- [["UcDsGsFsFN", null], ["BMJNwT", null], ["wU9dfM40pR", null], ["IrRr", null], ["izcO", null]]

eogo[a] <- [[-6.495], [-3.338], [0.0]]

mkfn[a, b, c, d] <- [[null, null, "BMJNwT", "BMJNwT"], [null, null, "IrRr", "IrRr"], [null, null, "UcDsGsFsFN", "UcDsGsFsFN"], [null, null, "izcO", "izcO"], [null, null, "wU9dfM40pR", "wU9dfM40pR"]]

ruff[a, b, c, d, e] <- [[-6.495, 'null', 'null', -6.495, -6.495], [-3.338, 'null', 'null', -3.338, -3.338], [0.0, 'null', 'null', 0.0, 0.0]]


ymne[A, A, A] := eogo[A]
nhyq[D, A, A, B, C, A] := ymne[C, A, D], ymne[B, -6.495, A]
cott[F, E, F, E, E, F, F, C] := ymne[B, A, C], ymne[D, C, B], kayy[E, F]
yemg[B, B, A] := kayy[A, B]
anly[D, C, A, B] := eogo[A], yemg[C, B, D], kayy[_, C], ge(5, sqrt(A))
sumu[F, A, B, B, F] := nhyq[D, B, B, B, A, F], ymne[E, A, F]
mwgn[B, A] := yemg[A, null, B]
sfso[B, A, A, D, B, D, D] := kayy[_, A], kayy[B, E], ymne[D, D, D]
eruo[M, E, G, F, L] := ruff[D, J, I, A, D], ruff[F, J, H, C, E], cott[G, L, G, M, L, K, K, F]
ywoo[C, A, B] := anly[A, B, C, B]
alqm[C, A, A, B] := mwgn[A, B], eogo[C], not sumu[C, C, C, C, C], lt(atanh(C), acos(C)), ge(1, rad_to_deg(C))
ymne[D, C, D] := eruo[B, C, F, C, A], ywoo[D, B, H], cott[G, A, G, A, B, F, H, C]
tlwb[C, C] := alqm[A, C, B, D]
ijem[E, G, F, E, F, D, B] := sfso[B, E, E, F, B, F, G], tlwb[B, "wU9dfM40pR"], tlwb[A, D]

cpoc[F, C, D, A, E] := ijem[A, C, C, A, C, E, E], sumu[C, C, D, C, D], mkfn[A, B, E, F]

?[a, b, c, d, e] := cpoc[a, b, c, d, e]

I got the following results on this program:

wU9dfM40pR	-6.495	-6.495	null	wU9dfM40pR

I also tried to get the values for ijem, sumu, and mkfn, which were the subgoals in the last rule, and got the following results:

# ?[a, b, c, d, e, f, g] := ijem[a, b, c, d, e, f, g]
null	-6.495	-6.495	null	-6.495	BMJNwT	wU9dfM40pR
null	-6.495	-6.495	null	-6.495	IrRr	wU9dfM40pR
null	-6.495	-6.495	null	-6.495	UcDsGsFsFN	wU9dfM40pR
null	-6.495	-6.495	null	-6.495	izcO	wU9dfM40pR
null	-6.495	-6.495	null	-6.495	wU9dfM40pR	wU9dfM40pR
null	-3.338	-3.338	null	-3.338	BMJNwT	wU9dfM40pR
null	-3.338	-3.338	null	-3.338	IrRr	wU9dfM40pR
null	-3.338	-3.338	null	-3.338	UcDsGsFsFN	wU9dfM40pR
null	-3.338	-3.338	null	-3.338	izcO	wU9dfM40pR
null	-3.338	-3.338	null	-3.338	wU9dfM40pR	wU9dfM40pR
null	0	0	null	0	BMJNwT	wU9dfM40pR
null	0	0	null	0	IrRr	wU9dfM40pR
null	0	0	null	0	UcDsGsFsFN	wU9dfM40pR
null	0	0	null	0	izcO	wU9dfM40pR
null	0	0	null	0	wU9dfM40pR	wU9dfM40pR


# ?[a, b, c, d, e] := sumu[a, b, c, d, e]
-6.495	-6.495	-6.495	-6.495	-6.495
0	0	0	0	0


# ?[a, b, c, d] := mkfn[a, b, c, d]
null	null	BMJNwT	BMJNwT
null	null	IrRr	IrRr
null	null	UcDsGsFsFN	UcDsGsFsFN
null	null	izcO	izcO
null	null	wU9dfM40pR	wU9dfM40pR

Then I use these values to construct an equivalent program, which only include the last rule:

mkfn[a, b, c, d] <- [
    [null, null, "BMJNwT", "BMJNwT"], 
    [null, null, "IrRr", "IrRr"], 
    [null, null, "UcDsGsFsFN", "UcDsGsFsFN"], 
    [null, null, "izcO", "izcO"], 
    [null, null, "wU9dfM40pR", "wU9dfM40pR"]
]

sumu[a, b, c, d, e] <- [[-6.495, -6.495, -6.495, -6.495, -6.495], [0.0, 0.0, 0.0, 0.0, 0.0]]

ijem[a, b, c, d, e, f, g] <- [
    [null, -6.495, -6.495, null, -6.495, "BMJNwT", "wU9dfM40pR"], 
    [null, -6.495, -6.495, null, -6.495, "IrRr", "wU9dfM40pR"], 
    [null, -6.495, -6.495, null, -6.495, "UcDsGsFsFN", "wU9dfM40pR"], 
    [null, -6.495, -6.495, null, -6.495, "izcO", "wU9dfM40pR"], 
    [null, -6.495, -6.495, null, -6.495, "wU9dfM40pR", "wU9dfM40pR"], 
    [null, -3.338, -3.338, null, -3.338, "BMJNwT", "wU9dfM40pR"], 
    [null, -3.338, -3.338, null, -3.338, "IrRr", "wU9dfM40pR"], 
    [null, -3.338, -3.338, null, -3.338, "UcDsGsFsFN", "wU9dfM40pR"], 
    [null, -3.338, -3.338, null, -3.338, "izcO", "wU9dfM40pR"], 
    [null, -3.338, -3.338, null, -3.338, "wU9dfM40pR", "wU9dfM40pR"], 
    [null, 0.0, 0.0, null, 0.0, "BMJNwT", "wU9dfM40pR"], 
    [null, 0.0, 0.0, null, 0.0, "IrRr", "wU9dfM40pR"], 
    [null, 0.0, 0.0, null, 0.0, "UcDsGsFsFN", "wU9dfM40pR"], 
    [null, 0.0, 0.0, null, 0.0, "izcO", "wU9dfM40pR"], 
    [null, 0.0, 0.0, null, 0.0, "wU9dfM40pR", "wU9dfM40pR"]
]

cpoc[F, C, D, A, E] := ijem[A, C, C, A, C, E, E], sumu[C, C, D, C, D], mkfn[A, B, E, F]
?[a, b, c, d, e] := cpoc[a, b, c, d, e]

But I got the following results, which were different from the original one:

wU9dfM40pR	-6.495	-6.495	null	wU9dfM40pR
wU9dfM40pR	0	0	null	wU9dfM40pR

As cpoc only appears once in the program, so I expect these two results should be the same.

(So sorry that this program is too big. This is already a reduced version, but I am still working on a simpler one, but there are some recursive queries in this program, so it is a little hard to reduce it.)

[zh217]

Ahh, this is a bit hard to debug. One thing though is that sumu is used in negation, and ijem depends on the negation of sumu indirectly through some other relations. So it is possible that those two programs are in fact not equivalent. But I'm not sure. (Edit: no, I have looked at the examples again and I think they really SHOULD be equivalent.)

Don't worry about the program being too big. If it is indeed a bug, it needs fixing. The worst thing a database can do is to give wrong outputs.

Meanwhile, there is a way to get more information:

1. Use the standalone server for your platform, and run it with the trace environment variable set up:

   RUST_LOG=cozo::query::eval=trace ./cozo-bin server
   

2. Connect to it from a Python client, and run the query
3. Now look at the terminal window, you should see every value produced by the query evaluator.

[zh217]

FYI these are the values at the strata boundary:

[2023-05-09T16:42:49Z TRACE cozo::query::eval] {eogo: EpochStore { total: Normal(RegularTempStore { inner: {[-6.495]: false, [-3.338]: false, [0]: false} }), delta: Normal(RegularTempStore { inner: {} }), use_total_for_delta: false, arity: 1 }, kayy: EpochStore { total: Normal(RegularTempStore { inner: {["BMJNwT", null]: false, ["IrRr", null]: false, ["UcDsGsFsFN", null]: false, ["izcO", null]: false, ["wU9dfM40pR", null]: false} }), delta: Normal(RegularTempStore { inner: {} }), use_total_for_delta: false, arity: 2 }, ruff: EpochStore { total: Normal(RegularTempStore { inner: {[-6.495, "null", "null", -6.495, -6.495]: false, [-3.338, "null", "null", -3.338, -3.338]: false, [0, "null", "null", 0, 0]: false} }), delta: Normal(RegularTempStore { inner: {} }), use_total_for_delta: false, arity: 5 }}
[2023-05-09T16:42:49Z TRACE cozo::query::eval] {eogo: EpochStore { total: Normal(RegularTempStore { inner: {[-6.495]: false, [-3.338]: false, [0]: false} }), delta: Normal(RegularTempStore { inner: {} }), use_total_for_delta: false, arity: 1 }, kayy: EpochStore { total: Normal(RegularTempStore { inner: {["BMJNwT", null]: false, ["IrRr", null]: false, ["UcDsGsFsFN", null]: false, ["izcO", null]: false, ["wU9dfM40pR", null]: false} }), delta: Normal(RegularTempStore { inner: {} }), use_total_for_delta: false, arity: 2 }, mkfn: EpochStore { total: Normal(RegularTempStore { inner: {[null, null, "BMJNwT", "BMJNwT"]: false, [null, null, "IrRr", "IrRr"]: false, [null, null, "UcDsGsFsFN", "UcDsGsFsFN"]: false, [null, null, "izcO", "izcO"]: false, [null, null, "wU9dfM40pR", "wU9dfM40pR"]: false} }), delta: Normal(RegularTempStore { inner: {} }), use_total_for_delta: false, arity: 4 }, sumu: EpochStore { total: Normal(RegularTempStore { inner: {[-6.495, -6.495, -6.495, -6.495, -6.495]: false} }), delta: Normal(RegularTempStore { inner: {} }), use_total_for_delta: false, arity: 5 }, yemg: EpochStore { total: Normal(RegularTempStore { inner: {[null, null, "BMJNwT"]: false, [null, null, "IrRr"]: false, [null, null, "UcDsGsFsFN"]: false, [null, null, "izcO"]: false, [null, null, "wU9dfM40pR"]: false} }), delta: Normal(RegularTempStore { inner: {} }), use_total_for_delta: false, arity: 3 }, ymne: EpochStore { total: Normal(RegularTempStore { inner: {[-6.495, -6.495, -6.495]: false, [-3.338, -3.338, -3.338]: false, [0, -6.495, 0]: false, [0, -3.338, 0]: false, [0, 0, 0]: false} }), delta: Normal(RegularTempStore { inner: {} }), use_total_for_delta: false, arity: 3 }}

It's a bit hard to read, but here sumu has only one tuple [-6.495, -6.495, -6.495, -6.495, -6.495] instead of two. Probably there is something wrong with the semi-naive rewrite: due to the presence of negation, the way sumu was evaluated was different for the two cases. That's the only place it could go wrong.

When I have some larger chunk of time I will try to disable the semi-naive rewriting and see if the result is the same. Then we can get a focus on what the problem really is.

On a side note, there is a new feature in the dev version of the Python client to generate query strings programmatically here. I think this might be of interest to you.

[zh217]

I've found the root cause. It's a bit hard to explain, but the following is a truly minimal example:

x[A] := A = 1
y[A, A] := A = 1
y[A, B] := A = 0, B = 1, x[B]

?[C] := y[A, _], y[C, A]

:disable_magic_rewrite true

The result should be 0 and 1, but the execution engine will miss the 0 (the :disable_magic_rewrite, which instructs the engine to execute the queries as written without rewriting, currently only works on dev builds). The example is minimal in the sense that changing anything at all (for example by writing x[] <- [[1]] instead) will produce the right result.

Technically, this is due to the implemented semi-naïve algorithm failing to handle a corner case where a relation is used multiple times within.

Regardless, a fix is on the way! Thanks so much for the finding, this bug is so convoluted that I don't think it will ever be noticed if one just casually looks at the results (but it will definitely produce wrong results in the real world when the queries become complicated enough).

[DerZc]

Hi @zh217

On a side note, there is a new feature in the dev version of the Python client to generate query strings programmatically here.

Thank you very much for your good advices, currently I am implementing a randomly Datalog generator, I will refer to your advice.

So happy this report is useful to you, I will debug the test case before report next time. Thank you for fixing it!

[DerZc]

The method we used to find this bug has been published at OOPSLA2024, this is the preprint version of our paper https://arxiv.org/abs/2402.12863