Ungrounded variables cannot be grounded by the magic sets transform

[arlencox]

In addition to being a performance optimization, the magic sets transform often grounds variables that might otherwise be ungrounded. Unfortunately, it appears that souffle performs a check for grounding prior to performing the magic sets transform and as a result cannot leverage this important aspect of the transform.

Consider the following example:

.decl fib(n: number, r: number) magic

fib(0, 0).
fib(1, 1).

fib(n, r1 + r2) :- n >= 2, fib(n-1, r1), fib(n-2, r2).

.decl result(r: number)
.output result

result(r) :- fib(30, r).

If I run this with souffle I get the following result:

$ souffle -D- fib.dl
Error: Ungrounded variable n in file fib.dl at line 6
fib(n, r1 + r2) :- n >= 2, fib(n-1, r1), fib(n-2, r2).
----^--------------------------------------------------
1 errors generated, evaluation aborted

However, if I apply the magic sets transformation manually, I get the following datalog file:

.decl fib_magic_bf(n: number)
.decl fib_bf(n: number, r: number)

fib_magic_bf(n-1) :- fib_magic_bf(n), n >= 2.
fib_magic_bf(n-2) :- fib_magic_bf(n), n >= 2, fib_bf(n-1, _).

fib_bf(0, 0) :- fib_magic_bf(0).
fib_bf(1, 1) :- fib_magic_bf(1).

fib_bf(n, r1+r2) :- fib_magic_bf(n), n >= 2, fib_bf(n-1, r1), fib_bf(n-2, r2).

.decl result(r: number)
.output result

fib_magic_bf(30).
result(r) :- fib_bf(30, r).

Not only is every variable grounded, but this version of fib terminates efficiently.

$ souffle -D- fib-magic.dl
---------------
result
r
===============
832040
===============

It seems that souffle's magic sets transformation should be able to accomplish this transformation.

My simple attempts at fixing this myself have failed. I cannot seem to find a place in the pipeline that I can place an unmodified magic sets transform that doesn't result in either an assertion violation or an ungrounded variable error.

These experiments were performed on release 2.2 as well as 7be1e61c1d9a70b4935f5b34138f0c1d61bd69ad, which was HEAD when I first encountered these problems in release 2.2.

[b-scholz]

This is a nice observation! But note that we cannot assume that all programs with ungrounded variables will become programs with grounded variables after applying the magic-set transform. It is an easier assumption that we assume that we have a program with grounded variables for the magic-set transformation.

In the above example, it may be easier to apply a linear transformation for the index expression, i.e.,

decl fib(n: number, r: number) magic

fib(0, 0).
fib(1, 1).

fib(n+1, r1 + r2) :- n >= 1, n <=30, fib(n, r1), fib(n-1, r2).  

.decl result(r: number)
.output result

result(r) :- fib(30, r).

also note you need an exit condition. Souffle is a bottom-up solver, i.e., the facts are added first to the relation and then rules are applied until no further change in the relations can be found. In your example, the fib series would never terminate.

[arlencox]

we cannot assume that all programs with ungrounded variables will become programs with grounded variables after applying the magic-set transform

Of course not! But this is why I think it would be interesting to check for grounding after applying the magic sets transform. It might become grounded, in which case there is no problem. If not, I guess the risk is that the error message might be worse due to it occurring later in the processing.

it may be easier to apply a linear transformation for the index expression

I'm aware. I tried a bunch of variants of this to see if there was one that worked. Ultimately, I don't care about solving fib. It's just a nice example to demonstrate the problem.

The actual problem is that we have to make all sorts of domain restrictions in our static analysis to ensure that it terminates when a magic sets transformation would suffice. As a result, the rules are harder to read and we're more likely to make a mistake in the domain restricting relation/rules -- particularly when we make an update to a rule and forget to update the domain rule.

I recognize that this isn't a necessary feature. It would just be nice and it seemed like, in the right hands, it would be almost trivial to solve.

[b-scholz]

Thinking more about your example, there are two aspects in your example that would need to be addressed separately.

(1) Ungrounded variables: They are caused by functors (in your example by addition/subtraction). As mentioned before, we can use a simple linear transformation to make variables grounded. Let's assume a predicate in the body of a rule. The transform is straight forward:

A(x+d, ...)  =>  A(y, ...),  y=x+d => A(y, ...),  x = y - d 

With this transformation you can make an ungrounded variable to a grounded variable. This transformation was already proposed here

https://github.com/souffle-lang/souffle/issues/1294

by @psubotic but not implemented. It is not much effort to implement this. I am happy to guide you implementing this transformation (NB: won't take too long).

(2) Termination: You have specified in your example an infinite sequence of Fibonacci numbers and the magic-set transform specialises the Fibonacci sequence to a finite one. This should work for constant parameters (like in your example) but does not work for all programs such as the following,

.decl fib,result(x:number)
fib(1). fib(2).
fib(n1+n2) :-  fib(n1), fib(n2).
result(n) :- fib(n), n<100. 
.output result

where there is a constraint (i.e., n <100) that is not propagated by the magic-set transform. Think of more complex constraints and contexts that magic-set cannot propagate; this is an example only.

The termination aspect is interesting and needs to be studied in more detail from a theoretical viewpoint. Souffle is a bottom-up solver and, hence, would get stuck computing all numbers of the Fibonacci sequence.

With magic-set transform, the sequence terminates because it will be specialised by the use of the result (in your example - it will be for index 30) but it fails in my example because the magic-set transform is not clever enough to propagate the context.

To summarise - magic-set transform was seen in the past as a way to improve performance but not as means to achieve termination. I am intrigued by this observation. I am happy to talk more about this - send me an email Bernhard.Scholz@sydney.edu.au