Incorrect computation with commit `778dfa1`

[bertram-gil]

Hi guys,

Consider the following program:

type fib(i32, i32)
type a__(i32, i32)
@demand("bf")
rel fib(x, a + b) = fib(x - 1, a), fib(x - 2, b), x > 1
rel fib = {(0, 1), (1, 1)}

rel a__ = {
	(35, 24),
	(91, 1),
	(44, 91),
	(48, 92),
	(6, 85),
}

rel a__(a, a) = fib(a, a)

query a__

When I run this program with the latest Scallop commit (778dfa126e98acb90a21dbececc825699f6688bd), I get:

$ ./scli program.scl
a__: {(1, 1), (6, 85), (35, 24), (44, 91), (48, 92), (91, 1)}

If I add another rule (rel a__(a, b) = a__(a, b), fib(b, b)) for relation a__ to get the following new program:

type fib(i32, i32)
type a__(i32, i32)
@demand("bf")
rel fib(x, a + b) = fib(x - 1, a), fib(x - 2, b), x > 1
rel fib = {(0, 1), (1, 1)}

rel a__ = {
	(35, 24),
	(91, 1),
	(44, 91),
	(48, 92),
	(6, 85),
}

rel a__(a, a) = fib(a, a)
rel a__(a, b) = a__(a, b), fib(b, b)
query a__

Now if I run this program, I get:

a__: {(1, 1), (2, 2), (3, 3), (6, 85), (35, 24), (44, 91), (48, 92), (91, 1)}

I get 2 extra tuples (2, 2) and (3, 3).
However, adding this rule for relation a__ should not add these extra tuples for a__.

Also note that fib for the first program is:

fib: {(0, 1), (1, 1)}

and for the second program:

fib: {(0, 1), (1, 1), (2, 2), (3, 3), (4, 5), (5, 8), (6, 13), (7, 21), (8, 34), (9, 55), (10, 89), (11, 144), (12, 233), (13, 377), (14, 610), (15, 987), (16, 1597), (17, 2584), (18, 4181), (19, 6765), (20, 10946), (21, 17711), (22, 28657), (23, 46368), (24, 75025), (25, 121393), (26, 196418), (27, 317811), (28, 514229), (29, 832040), (30, 1346269), (31, 2178309), (32, 3524578), (33, 5702887), (34, 9227465), (35, 14930352), (36, 24157817), (37, 39088169), (38, 63245986), (39, 102334155), (40, 165580141), (41, 267914296), (42, 433494437), (43, 701408733), (44, 1134903170), (45, 1836311903), (46, -1323752223), (47, 512559680), (48, -811192543), (49, -298632863), (50, -1109825406), (51, -1408458269), (52, 1776683621), (53, 368225352), (54, 2144908973), (55, -1781832971), (56, 363076002), (57, -1418756969), (58, -1055680967), (59, 1820529360), (60, 764848393), (61, -1709589543), (62, -944741150), (63, 1640636603), (64, 695895453), (65, -1958435240), (66, -1262539787), (67, 1073992269), (68, -188547518), (69, 885444751), (70, 696897233), (71, 1582341984), (72, -2015728079), (73, -433386095), (74, 1845853122), (75, 1412467027), (76, -1036647147), (77, 375819880), (78, -660827267), (79, -285007387), (80, -945834654), (81, -1230842041), (82, 2118290601), (83, 887448560), (84, -1289228135), (85, -401779575), (86, -1691007710), (87, -2092787285), (88, 511172301), (89, -1581614984), (90, -1070442683), (91, 1642909629), (92, 572466946)}

Please let me know if you cannot reproduce this result or if I am doing something wrong.

My machine:

   Operating System: Debian GNU/Linux 10 (buster)  
   Kernel: Linux 5.4.188.1.amd64-smp
   Architecture: x86-64

[Liby99]

For this one, I have two comments after investigating the issue:

1. To me, there is no error in getting this result. The logic goes as follows:

The demand("bf") attribute will tell Scallop to compute fib in an on-demand basis. Due to that a__ relation containing up-to 92 for the second element, Scallop needs to know the fib relation up to the first element being 92. This will in turn populate the whole fib relation to contain all the x from 0 to 92, hence the long fib relation you see from running the second program.

This is expected, as adding demand will have side-effects on information propagation. Now a__ and fib cannot be treated as two separated relations. There will be information passing between these two relations.

At the end, since fib now contains all these tuples, it appears that (1, 1), (2, 2), and (3, 3) are the three tuples that match the atom fib(a, a). Therefore by the rule

rel a__(a, a) = fib(a, a)

we will add these tuples into the a__ relation as well.

2. There is actually error in the integer overflow. Apparently fib(92) is a pretty large number, and this will cause integer overflow, hence the negative numbers you see in fib. When compiling scli, I have the runtime overflow check being disabled for performance. But using scli with debug mode will actually throw error. A quick fix to this is setting the type of fib and a__ to i128 (i64 is still not big enough). Otherwise, I'm thinking about a better way to raise the error to the user.

[bertram-gil]

Thanks for the explanation! :)
So then it seems that the first program is the buggy one? Tuples (2, 2) and (3, 3) are then missing from the result of the first program?

[Liby99]

No. Again since we are touching the domain of magic-set transformation/demand transformation, things would start to get trickier and you wouldn't be able to tackle the problem using the old assumptions you have.

Here, we have defined fib saying it should be demand transformed. Therefore we will only do computation if there is a demand on fib with the pattern "bound-free" (bf). In the first program, the rule a__(a, a) = fib(a, a) does not populate a demand for fib with the pattern "bound-free". At the end, there is no demand on fib and so fib won't be computed. Therefore only the base-cases will be populated (0, 1), (1, 1).

For example,

• :- fib(3, a) creates a demand on fib with the "bound-free" pattern: the first argument is bounded and is 3.
• :- d(a), fib(a, b) creates a demand on fib with the "bound-free" pattern: the first argument is bounded by any argument a in the relation d.
• If you simply have :- fib(a, b) the argument a is not bounded by any.