Removing "Auto-increment functor in a recursive rule" error.

[thomas-colcombet]

Hi,

I would like to use autoinc() in a recursive rule, but in a situation for which I know in advance that no infinite recursion can happen. Is there a way to disable the error message "Auto-increment functor in a recursive rule", either globally, or for a specific rule?

[quentin]

Hi, this check cannot be disabled.
Do you have a workaround or would like to share a minimized example of such a rule ?

[thomas-colcombet]

Hi,

There is a workaround, yes, which requires more effort for producing the souffle code.

Here would be a simple example (though not very narrative):

.type node <: number
.type myid <: number

.decl start()
.decl b(n:node,child1:node,child2:node,source:myid)

start().
b(autoinc(),autoinc(),autoinc(),"1") :- start().
b(n,autoinc(),autoinc(),"2") :- b(_,n,_,"1").
b(n,autoinc(),autoinc(),"2") :- b(_,_,n,"1").
b(n,autoinc(),autoinc(),"3") :- b(_,n,_,"2").
b(n,autoinc(),autoinc(),"3") :- b(_,_,n,"2").
b(n,autoinc(),autoinc(),"4") :- b(_,n,_,"3").
b(n,autoinc(),autoinc(),"4") :- b(_,_,n,"3").

Here one should imagine that "1", "2", "3", "4" are more complex objects that arise from the problem (such as line numbers, function names, or combinations).
This code constructs a binary tree of height 4.

The above code cannot be executed because of the of recursive rule error. The abvious workaround is:

.type node <: number
.type myid <: number

.decl start()
.decl b1(n:node,child1:node,child2:node)
.decl b2(n:node,child1:node,child2:node)
.decl b3(n:node,child1:node,child2:node)
.decl b4(n:node,child1:node,child2:node)

start().
b1(autoinc(),autoinc(),autoinc()) :- start().
b2(n,autoinc(),autoinc()) :- b1(_,n,_).
b2(n,autoinc(),autoinc()) :- b1(_,_,n).
b3(n,autoinc(),autoinc()) :- b2(_,n,_).
b3(n,autoinc(),autoinc()) :- b2(_,_,n).
b4(n,autoinc(),autoinc()) :- b3(_,n,_).
b4(n,autoinc(),autoinc()) :- b3(_,_,n).

But in some context, it is more complicated to produce the second code, since it requires to make explicit the reason why it should terminate, ie make beforehand the dependency analysis, and rename by hand all the non-terminals. Hence my question, since I believe the Souffle engine would be able to execute the first code without noticing it, if the recursive rule error was not issued.

[quentin]

If you know the whole tree in advance, can you provide the unique identifiers of nodes as literals directly and not depend on autoinc at all ?

b(1,2,3,"1").
b(2,4,5,"2").
b(3,6,7,"2").
...

Otherwise, to stick to your original question, I would generate unique node string identifiers and then use ord(string) to create unique numeric identifiers. The root node is named root and other nodes identifiers are a sequence of l and r (chosen arbitrarily to represent left and right child):

.type node <: number
.type myid <: symbol

.decl b(n:symbol, lhs:symbol, rhs:symbol, id:myid)
b("root", "l", "r", "1").
b(n, cat(n,"l"), cat(n,"r"), "2") :- b(_,n,_,"1").
b(n, cat(n,"l"), cat(n,"r"), "2") :- b(_,_,n,"1").

b(n, cat(n,"l"), cat(n,"r"), "3") :- b(_,n,_,"2").
b(n, cat(n,"l"), cat(n,"r"), "3") :- b(_,_,n,"2").

b(n, cat(n,"l"), cat(n,"r"), "4") :- b(_,n,_,"3").
b(n, cat(n,"l"), cat(n,"r"), "4") :- b(_,_,n,"3").

.decl bi(n:node, lhs:node, rhs:node, id:myid)
bi(ord(n), ord(lhs), ord(rhs), id) :-
  b(n, lhs, rhs, id).

.output b()
.output bi()

output:

---------------
b
n       lhs     rhs     id
===============
root    l       r       1
l       ll      lr      2
r       rl      rr      2
ll      lll     llr     3
lr      lrl     lrr     3
rl      rll     rlr     3
rr      rrl     rrr     3
lll     llll    lllr    4
llr     llrl    llrr    4
rll     rlll    rllr    4
rlr     rlrl    rlrr    4
lrl     lrll    lrlr    4
lrr     lrrl    lrrr    4
rrl     rrll    rrlr    4
rrr     rrrl    rrrr    4
===============
---------------
bi
n       lhs     rhs     id
===============
0       1       2       1
1       7       8       2
2       9       10      2
7       11      12      3
8       15      16      3
9       13      14      3
10      17      18      3
11      19      20      4
12      27      28      4
13      23      24      4
14      31      32      4
15      21      22      4
16      29      30      4
17      25      26      4
18      33      34      4
===============

Note that ord(...) provides a unique number for each string, but in general do not assume it to be deterministic.

[thomas-colcombet]

Thank you for your answer.
Yet, now I am puzzled.

Indeed, the recursive rule error seems to exist for avoiding non-termination in situation such as:

.decl a(n: number)
a(autoinc()) :- a(_).
a(-1).

(and indeed, souffle complains)

However, using cat, the exact same non-termination effect arises:

.decl a(s: symbol)
.output a(IO=stdout)
a(cat("o",s)) :- a(s).
a("").

Which does not terminate when executed.

Hence, I do not understand the rationale behind forbidding the first code, and allowing the second one. Both situations seems to me of the same nature...

[quentin]

There is probably no rationale, there is a lot of space for semantics checking improvements.