I would like to define the set of nodes in a directed graph reachable from all nodes in a given set of start nodes in Clingo. To my understanding, this can be done via conditions in a rule body: in a rule
p(X) :- q(X) : r(X).
a conjunction of rules q(a) is dynamically generated in the body of p/1 for grounded facts a, for which the rule r(a) also holds. Now for some reason, the following set of rules results in an "unsafe" variable X being discovered on the last line:
% Test case
arc(1,4). arc(2,4). arc(3,5). arc(4,1). arc(4,2). arc(4,3).
start(1). start(4). start(5).
% Define a path inductively, with the base case being path of length 1:
path(A, B) :- arc(A, B).
path(A, B) :- arc(A, X), arc(X, B).
path(A, B) :- arc(A, X), path(X, Y), arc(Y, B).
% A node X is simply reachable/1, if there is a possibly empty path to it
% from a start node or reachable/2 from A, if there is a path to it from A:
reachable(X) :- start(X).
reachable(X) :- start(A), path(A, X).
reachable(X, A) :- path(A, X).
% Predicate all_reach defined by the reachable relation:
all_reach(X) :- reachable(X, A) : start(A).
I wanted to ask, what is meant by an "unsafe" variable, and how might I amend this situation? One source claims that an unsafe variable is a variable, which appears in the head of a rule but not in the body, which makes sense as the symbols :- denote a reverse implication. However, this does not seem to be the case here, so I'm confused.
Could it be that there might not be a grounded fact a for which start(a) holds, and hence the body of the implication or rule becomes empty, causing the unsafety. Is that it? Is there a standard way of avoiding this?
The issue was that there wasn't a positive rule in the body of all_reach/1 that was satisfied for at least some grounded instance of X. Adding the lines
% Project nodes from arcs
node(X) :- arc(X,Y).
node(Y) :- arc(X,Y).
and reformulating the all_reach/1 rule as
all_reach(X) :- reachable(X, A) : start(A); node(X).
solved the issue. The desired conjunction
∧[i=1 → ∞] reachable(d, s[i])
for all start nodes s[i] and destination nodes d is then generated as the
body of allreach/1.
In other words, when using conditionals in the body b/m of a rule r/n,
there must still be a predicate p in b that is unconditionally grounded
for any variables present in the head of the rule. Otherwise we might end up
with an ambiguity or an ever-expanding rule during grounding, which is unsafe.