potassco / clingo

🤔 A grounder and solver for logic programs.
https://potassco.org/clingo
MIT License
616 stars 81 forks source link

Unsafety in conditional rules and fixing them #347

Closed SeSodesa closed 2 years ago

SeSodesa commented 2 years ago

Hello there.

Not sure if this is the right place to ask for usage tips, but I have a bit of a conundrum and the user manual only has one instance of the word unsafe in it, in chapter 6.1. I am trying to declare a conditional or dynamically expanded rule of the form

p(X) :- q(X, A) : r(A).

but Clingo is reporting the variable X as "unsafe":

Reading from test.lp
test.lp:31:1-52: error: unsafe variables in:
  p(X):-[#inc_base];q(X, A):r(A).
test.lp:31:3-4: note: 'X' is unsafe

*** ERROR: (clingo): grounding stopped because of errors
UNKNOWN

Why is this? One source by Lifschitz claims that

Some error messages say that the program has “unsafe variables.” Such a message usually indicates that the head of one of the rules includes a variable that does not occur in its body; …

However, this does not seem to be the case here. How might I fix a problem like this?

SeSodesa commented 2 years ago

Never mind. Adding an unconditionally grounded rule s(X) after the conditional worked:

p(X) :- q(X, A) : r(A); s(X).

I guess ambiguities are bad?

rkaminsk commented 2 years ago

It is important to provide a binding for X. Consider the program

d(f(1)).
p(X) :- q(X) : #false.

The conditional literal is true for all values of X. We obtain an infinite answer set:

d(f(1)), p(1), p(f(1)), p(f(f(1))), ...