Recursion sub-graph with Aggregates in the Body

[stephanzwicknagl]

How to deal with recursive sub-graphs of rules with aggregates in the body?

Recursion sub-graphs are generated at transformations that have positive recursion, meaning that a rule's dependent also occurs in a non-negated literal in the body of the rule (or an equivalent dependency of multiple rules of a component).

Positive recursion is recognized by using the positive-dependency graph. It is equivalent to the normal dependency graph in the way that it connects dependents and conditions of rules. It only uses conditions that positive conditions to build the graph. A recursion is found if there is a loop or strongly connected component of in the positive-dependency graph.

Positive conditions literals in the body of a rule that are non-negated and do not occur inside an aggregate. The latter is due to the more complex process of determining a condition being positive or negative in combination with aggregates (see below). For a simple, correct solution, the child literals of aggregates in the body of the rule should not be considered positive conditions.

Example without recursion

reached(V) :- reached(U), hc(U,V), not start(V).

• reached/1 is a dependent of the rule
• reached/1 is a condition and a positive condition of the rule
• hc/2 is a condition and a positive condition of the rule
• start/1 is a condition, but not a positive condition of the rule

The positive-dependency graph contains a loop at this rule due to the positive condition reached/1.

The corresponding recursion justification program for building the sub-graph:

#program iterate(n).
h(n, reached(V), (reached(U), hc(U,V))) :- model(reached(U)), model(hc(U,V)), not model(start(V)), not model(reached(V)).
model(@new()).

Example with recursion 1

reached(V) :- reached(U), 0 < #count{1,U,V: hc(U,V) }.

• reached/1 is a dependent of the rule
• reached/1 is a condition and a positive condition of the rule
• hc/2 is a condition, but not a positive condition of the rule
• start/1 is a condition, but not a positive condition of the rule

The positive-dependency graph does contain a loop.

The corresponding recursion justification program for building the sub-graph:

#program iterate(n).
h(n, reached(V), (reached(U), hc(U,V))) :- model(reached(U)), 0 < #count{1,U,V: model(hc(U,V))}, not model(reached(V)).
model(@new()).

Example with recursion 2

reached(V) :- 0 < #count{1,U: reached(U)}, hc(U,V), not start(V).

• reached/1 is a dependent of the rule
• reached/1 is a condition, but not a positive condition of the rule
• hc/2 is a condition and a positive condition of the rule
• start/1 is a condition, but not a positive condition of the rule

The positive-dependency graph does not contain a loop and a sub-graph should not be generated.

Determining positive or negative condition in aggregate

Take for example the rule
a(X) :- b(X), X<=#sum{Y:a(Y)}.

Here, it is not clear whether a positive condition exists with a/1. A positive condition exists for positive numbers Y in a(Y), but a negative condition exists for negative numbers.

How to find out if a literal in an aggregate is a positive condition?