Existentials

[seanmcl]

Consider the following program

.decl natural_number(x:number)
natural_number(0).
natural_number(x+1) :- natural_number(x), x < 10000000.

.decl query()
 query() :- natural_number(Y).

.output query(IO=stdout)

query is "true" if there exists some natural number. Souffle spends a long time building the huge table, when it only needs a single value. The magic set transform doesn't help this case either. Even changing the query to

 query() :- natural_number(0).

generates a big table. Our program is full of such cases. Is there any way to make souffle search for existentials like this more cleverly?

Thanks.

[psubotic]

Thinking out loud : you can make a small improvement by back-propagating the nulllaries where possible:

so say G is very large and as a consequence P is also large due to the following datalog program:

P(x, z) :- G(x, y), H(y, z). Q() :- P(x, z).

R(x, y) :- G(x, y)

So this could be rewritten as:

R(x, y) :- G(x, y). Q() :- P() P() :- G(x, y), H(y, z).

You however cant go further because 1. R uses G in its body and 2. P is defined by G(x, y), H(y, z) which has a bound vars., i.e., G.2 = H.1. If you ignore 2 you will not have completness (you essentially are computing in an abstract domain).

Perhaps Abduls work already does this?

On Fri, Jan 5, 2018 at 10:48 AM, Sean McLaughlin notifications@github.com wrote:

Consider the following program

.decl natural_number(x:number) natural_number(0). natural_number(x+1) :- natural_number(x), x < 10000000.

.decl query() query() :- natural_number(Y).

.output query(IO=stdout)

query is "true" if there exists some natural number. Souffle spends a long time building the huge table, when it only needs a single value. The magic set transform doesn't help this case either. Our program is full of such cases. Is there any way to make souffle search for existentials like this more cleverly?

Thanks.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/souffle-lang/souffle/issues/536, or mute the thread https://github.com/notifications/unsubscribe-auth/AAW3OZaFs4bQSSXEjXQPZIsF-mGhS54Mks5tHWNEgaJpZM4RT26B .

[b-scholz]

The magic set transformation would not help in this case because no constraints can be propagated.

However, we observe something specific in the given example. The point is that we just need to compute the base-cases for a relation to show the existence of a solution. The table natural_number would contain only a single element 0 in the table.

We could transform the input program to following optimised program:

.decl natural_number(x:number)
natural_number(0).
// removed because inductive: natural_number(x+1) :- natural_number(x), x < 10000000.

.decl query()
 query() :- natural_number(Y).

.output query(IO=stdout)

with the reasoning that if there are base-cases that produce tuples, than there exists a solution, and inductive rules will not contribute to the existence. Conversely, if there don't exist pairs from the base cases, the inductive rules cannot produce any tuples.

Note for each existence query, a specialised version of the relations on the right-hand side need to be produced.

[b-scholz]

@seanmcl - could you give us a real test case for this optimisation?

[b-scholz]

I forgot to say that the generalisation of this optimisation is given by any predicate on the right-hand side that has the format

A(_,...,_)

where all variables in its argument are unnamed. This predicate is an existential one and can be transformed to

qA()

and

qA() :- newA(_)

where newA() is a relation that contains non-recursive rules of A() only.

This optimisation is only useful if predicate A has no other use except the existential use.