5 ms·

Most modern datalogs, this one included, support negation, with some limitations.

YeGoblynQueenne 6y ago
Well, of course you can have negation and functions in "a" datalog language (there are different variants) but the point is that bottom-up evaluation is not then decidable. Out of curiosity, what kind of negation do you mean? Negation as failure or classical negation? And what do you mean about limitations?
- kragen 6y ago
  Hmm, I thought stratifying Datalog allowed bottom-up evaluation to remain decidable despite the presence of negation? And surely there are at least some kinds of functions that would also preserve deciability, even without stratification? I admit I don't know very much about Datalog, and I know you know a substantial amount, so maybe I'm just confused. But I'd like to understand how.
  - YeGoblynQueenne 6y ago
    Eh, to be honest I don't really know a substantial amount about Datalog. My specialty is Inductive Logic Programming and I'm interested in Datalog because it's decidability makes it a convenient represantation language for machine-learned logic programs. A very simple version of Datalog is sufficient for my purposes so I haven't really dabbled much in variations or more modern versions. So I might well be wrong about decidability depending on the absence of negation. Now that I think of it again, the problem with negation, in particular the negation-as-failure (NAF) in Prolog, is that it breaks the monotonicity of inference. Monotonicity in this context means that the model of a logic program (the set of facts that are immediate consequences of the facts and rules in the program, and that are derived in a bottom-up fashion with a TP operator, in let's say "traditional" Datalog) can only increase with the introduction of new facts. With NAF, this is not the case -introduction of a new fact may make a previously derived true fact now false. So maybe the problem with negation, at least NAF, is that it breaks the soundness of the inference procedure because facts already derived as true become false when new facts are derived. I give a (very crude, sorry) example of how Datalog's bottom-up evaluation works in an earlier comment: https://news.ycombinator.com/item?id=26522737 https://news.ycombinator.com/item?id=26522737 In short, bottom-up evaluation proceeds in discrete steps where at each step a new set of facts is derived from the facts and rules known so-far. Newly derived facts are added to the program so the set of facts in the program increases until no new facts can be derived. Without NAF, when a new set of facts is derived and added to the program, the truth value of already derived facts cannot change. But _with_ NAF, bottom-up evaluation may introduce a new fact in step k that makes a fact derived in step k - j false. So now we have an unsound derivation procedure. I wonder if this unsoundness actually translates to undecidability. Suppose the above happens - we introduce a new fact A and some existing fact B becomes false. What can we do to avoid this? Well, we can't know the truth value of B after the derivation of A before actually deriving A (because we don't know the truth of A before we can derive it), so we can't avoid deriving A. What we can do is go back and re-evaluate the truth of each derived fact, find that B is now false, and remove it from the program. But what if removing B allows a new fact, C, to be derived which was previously false because of B, and C is such that A is now false? Well, A cannot be derived given C, and without A we must derive B. Which means we have to get rid of C again and allow A back in. So now we're stuck in a loop. I don't know if this is actually something that can happen or not, I was just thinking through the problem right now given your question, so I may be talking nonsense. In any case, if there is such a problem with NAF, then maybe modern datalogs have a different negation scheme, allowing classical negation (as does Answer Set Programming). But I really don't know about that, hence my question to the OP about the kind of negation they mean. Which was a genuine question btw! I really don't know how modern Datalogs work. Anyway I'll go check a few sources and see if my sketch proof of undecidability above makes any sense and I'll come back to let you know what I find :)
    - YeGoblynQueenne 6y ago
      So this might take a while- there is a lot of literature on datalog variants with and without negation or recursion etc. I will have to check with some coleagues. I'll try to come back to you by Tuesday the latest. In the mean time you might find the following reference useful (or not because it's typically thick in opaque notation): http://webdam.inria.fr/Alice/ http://webdam.inria.fr/Alice/ It's a textbook on databases. There are several chapters on datalog, including negation and recursion which may be of some help, but so far I can't form an intuition about when datalog is decidable with negation. I think it is, but with restrictions e.g. stratification, as you say, or restricting to non-recursive programs, disallowing nonmonotonic updates (as in my sketch proof above) etc. Indeed, it's a bit frustrating because the literature seems to be endlessly fragmented into sub-languages with different properties that are difficult to summarise concisely and I could just not find a straightforward answer "this works" as far as I looked (which was a couple of hours since I left my previous comment). As I say in my comment above, there is a substantial amount I _don't_ know about datalog :)
      - YeGoblynQueenne 6y ago
        Ouch. There's 6 upvotes on this comment which I take to mean there's (at least) 6 people waiting to hear what I come up with. Unfortunately dear co-HN'ers I've come back to you empty-handed (and two days late... oh god). I contacted a colleague who is much more knowledgeable about bottom-up evaluation than me but I haven't heard back yet and that contact, plus my light reading of sources is really 90% of the bandwidth I have to devote to this right now. I have a paper deadline on the first of May that necessarily has to take up most of my brain. If any of you 6 (or anyone else!) is still interested by that time, please email me at the email in my sig and I'll be happy to dig further then, because this is something I'm actually intersted, too. Sorry for letting everyone down.
        kragen 6y ago
        You're not letting us down! We're collaboratively exploring a fascinating space of promising ideas! Please don't feel obligated to answer the following before May, or even read it. I didn't realize the space of Datalogs was so broad—I had thought that there was a single "stratified semantics" that was the standard. The stratified semantics that I knew about permits bottom-up evaluation with negation as failure to be decidable by putting negations of any predicate X/n into a stratum strictly higher than X/n (which is evaluated later), and non-negated consequences of X/n into a stratum equal to or higher than X/n's stratum. Like, as I understand it, if we have foo(X) :- bar(X), \+ baz(X, 3). quux(X) :- foo(X). then we put baz/2 in a lower stratum than foo/1, and quux/1 in a stratum not lower than foo/1. That way, by the time we are trying to infer foo/1 facts and quux/1 facts, we've already finished inferring all the baz/2 facts. Then, there's no way that we can infer more baz/2 facts in the future that could invalidate our foo/1 or quux/1 inferences. And this avoids the kind of non-monotonic loop you're talking about: if inferring fact A invalidates the inference of fact B, then B is in a strictly higher stratum than A, so we haven't inferred B yet at the time that we infer A. I think that with unrestricted negation the inconsistency or nontermination problem you mention does exist, in which there exists no (consistent) model for a program (is that the right terminology?); the simplest example would be: epimenides :- \+ epimenides. The stratification restriction avoids this because it would require the stratum of epimenides/1 to be strictly greater than itself, which a standard CLP(FD) solver like SWI-Prolog's will easily tell you cannot be done: ?- use_module(library(clpfd)). % library(error) compiled into error 0.00 sec, 17,872 bytes % library(apply) compiled into apply 0.00 sec, 29,088 bytes % library(assoc) compiled into assoc 0.00 sec, 36,240 bytes % library(lists) compiled into lists 0.00 sec, 25,304 bytes % library(pairs) compiled into pairs 0.00 sec, 9,040 bytes % library(clpfd) compiled into clpfd 0.03 sec, 736,792 bytes true. ?- X #> X. false. I think there's an additional problem as well, corresponding to Henkin sentences—programs for which models do exist, but for which there is no unique minimal model. For example, we could try to formalize George W. Bush's foreign policy: withUs(You) :- person(You), \+ withTheTerrorists(You). withTheTerrorists(You) :- person(You), \+ withUs(You). person(chirac). Now we have two minimal models, one in which person(chirac), withUs(chirac) and one in which person(chirac), withTheTerrorists(chirac). (Thus we can explain Freedom Fries, one of the most ridiculous and terrifying aspects of the politics of the early 02000s.) Further inference rules might rule out one, the other, or both of these models. In the same way, the stratification rule rejects this program: withUs/1 needs to be above (evaluated later than) withTheTerrorists/1, but also vice versa. I'm not sure how to state this so SWIPL's CLP(FD) can tell that it's unsolvable, but that's probably because I'm a total noob at logic in general: ?- X #> Y, Y #> X. X#=<Y+ -1, Y#=<X+ -1. ?- X #> Y, Y #> X, label([X, Y]). ERROR: Arguments are not sufficiently instantiated Of course it is not a hard problem to assign strata—a straightforward topological sort will immediately reject the loop. The stratification rule is conservative, though; not only will it reject all the undecidable problems, it will also reject some programs where a unique minimal model does exist; as a trivial example: withUs(chirac). withUs(You) :- person(You), \+ withTheTerrorists(You). withTheTerrorists(You) :- person(You), \+ withUs(You). person(chirac). So it makes sense that people would look for looser restrictions that still guarantee decidability. Anyway, that's my understanding of the situation! I might be mistaken about basic things. Thanks for the reference to the book! It looks great and I'll try to read it. Or, I guess, work through it.
namibj 6y ago
The notably limitation being that you can't combine negation and recursion.
- YeGoblynQueenne 6y ago
  Thanks, I think that's the main intuition to draw from this. But I figured OP (kragen) wanted to understand the why, also.
  - kragen 6y ago
    Indeed!

Well, of course you can have negation and functions in "a" datalog language (there are different variants) but the point is that bottom-up evaluation is not then decidable. Out of curiosity, what kind of negation do you mean? Negation as failure or classical negation? And what do you mean about limitations?

kragen 6y ago
Hmm, I thought stratifying Datalog allowed bottom-up evaluation to remain decidable despite the presence of negation? And surely there are at least some kinds of functions that would also preserve deciability, even without stratification? I admit I don't know very much about Datalog, and I know you know a substantial amount, so maybe I'm just confused. But I'd like to understand how.
- YeGoblynQueenne 6y ago
  Eh, to be honest I don't really know a substantial amount about Datalog. My specialty is Inductive Logic Programming and I'm interested in Datalog because it's decidability makes it a convenient represantation language for machine-learned logic programs. A very simple version of Datalog is sufficient for my purposes so I haven't really dabbled much in variations or more modern versions. So I might well be wrong about decidability depending on the absence of negation. Now that I think of it again, the problem with negation, in particular the negation-as-failure (NAF) in Prolog, is that it breaks the monotonicity of inference. Monotonicity in this context means that the model of a logic program (the set of facts that are immediate consequences of the facts and rules in the program, and that are derived in a bottom-up fashion with a TP operator, in let's say "traditional" Datalog) can only increase with the introduction of new facts. With NAF, this is not the case -introduction of a new fact may make a previously derived true fact now false. So maybe the problem with negation, at least NAF, is that it breaks the soundness of the inference procedure because facts already derived as true become false when new facts are derived. I give a (very crude, sorry) example of how Datalog's bottom-up evaluation works in an earlier comment: https://news.ycombinator.com/item?id=26522737 https://news.ycombinator.com/item?id=26522737 In short, bottom-up evaluation proceeds in discrete steps where at each step a new set of facts is derived from the facts and rules known so-far. Newly derived facts are added to the program so the set of facts in the program increases until no new facts can be derived. Without NAF, when a new set of facts is derived and added to the program, the truth value of already derived facts cannot change. But _with_ NAF, bottom-up evaluation may introduce a new fact in step k that makes a fact derived in step k - j false. So now we have an unsound derivation procedure. I wonder if this unsoundness actually translates to undecidability. Suppose the above happens - we introduce a new fact A and some existing fact B becomes false. What can we do to avoid this? Well, we can't know the truth value of B after the derivation of A before actually deriving A (because we don't know the truth of A before we can derive it), so we can't avoid deriving A. What we can do is go back and re-evaluate the truth of each derived fact, find that B is now false, and remove it from the program. But what if removing B allows a new fact, C, to be derived which was previously false because of B, and C is such that A is now false? Well, A cannot be derived given C, and without A we must derive B. Which means we have to get rid of C again and allow A back in. So now we're stuck in a loop. I don't know if this is actually something that can happen or not, I was just thinking through the problem right now given your question, so I may be talking nonsense. In any case, if there is such a problem with NAF, then maybe modern datalogs have a different negation scheme, allowing classical negation (as does Answer Set Programming). But I really don't know about that, hence my question to the OP about the kind of negation they mean. Which was a genuine question btw! I really don't know how modern Datalogs work. Anyway I'll go check a few sources and see if my sketch proof of undecidability above makes any sense and I'll come back to let you know what I find :)
  - YeGoblynQueenne 6y ago
    So this might take a while- there is a lot of literature on datalog variants with and without negation or recursion etc. I will have to check with some coleagues. I'll try to come back to you by Tuesday the latest. In the mean time you might find the following reference useful (or not because it's typically thick in opaque notation): http://webdam.inria.fr/Alice/ http://webdam.inria.fr/Alice/ It's a textbook on databases. There are several chapters on datalog, including negation and recursion which may be of some help, but so far I can't form an intuition about when datalog is decidable with negation. I think it is, but with restrictions e.g. stratification, as you say, or restricting to non-recursive programs, disallowing nonmonotonic updates (as in my sketch proof above) etc. Indeed, it's a bit frustrating because the literature seems to be endlessly fragmented into sub-languages with different properties that are difficult to summarise concisely and I could just not find a straightforward answer "this works" as far as I looked (which was a couple of hours since I left my previous comment). As I say in my comment above, there is a substantial amount I _don't_ know about datalog :)
    - YeGoblynQueenne 6y ago
      Ouch. There's 6 upvotes on this comment which I take to mean there's (at least) 6 people waiting to hear what I come up with. Unfortunately dear co-HN'ers I've come back to you empty-handed (and two days late... oh god). I contacted a colleague who is much more knowledgeable about bottom-up evaluation than me but I haven't heard back yet and that contact, plus my light reading of sources is really 90% of the bandwidth I have to devote to this right now. I have a paper deadline on the first of May that necessarily has to take up most of my brain. If any of you 6 (or anyone else!) is still interested by that time, please email me at the email in my sig and I'll be happy to dig further then, because this is something I'm actually intersted, too. Sorry for letting everyone down.
      - kragen 6y ago
        You're not letting us down! We're collaboratively exploring a fascinating space of promising ideas! Please don't feel obligated to answer the following before May, or even read it. I didn't realize the space of Datalogs was so broad—I had thought that there was a single "stratified semantics" that was the standard. The stratified semantics that I knew about permits bottom-up evaluation with negation as failure to be decidable by putting negations of any predicate X/n into a stratum strictly higher than X/n (which is evaluated later), and non-negated consequences of X/n into a stratum equal to or higher than X/n's stratum. Like, as I understand it, if we have foo(X) :- bar(X), \+ baz(X, 3). quux(X) :- foo(X). then we put baz/2 in a lower stratum than foo/1, and quux/1 in a stratum not lower than foo/1. That way, by the time we are trying to infer foo/1 facts and quux/1 facts, we've already finished inferring all the baz/2 facts. Then, there's no way that we can infer more baz/2 facts in the future that could invalidate our foo/1 or quux/1 inferences. And this avoids the kind of non-monotonic loop you're talking about: if inferring fact A invalidates the inference of fact B, then B is in a strictly higher stratum than A, so we haven't inferred B yet at the time that we infer A. I think that with unrestricted negation the inconsistency or nontermination problem you mention does exist, in which there exists no (consistent) model for a program (is that the right terminology?); the simplest example would be: epimenides :- \+ epimenides. The stratification restriction avoids this because it would require the stratum of epimenides/1 to be strictly greater than itself, which a standard CLP(FD) solver like SWI-Prolog's will easily tell you cannot be done: ?- use_module(library(clpfd)). % library(error) compiled into error 0.00 sec, 17,872 bytes % library(apply) compiled into apply 0.00 sec, 29,088 bytes % library(assoc) compiled into assoc 0.00 sec, 36,240 bytes % library(lists) compiled into lists 0.00 sec, 25,304 bytes % library(pairs) compiled into pairs 0.00 sec, 9,040 bytes % library(clpfd) compiled into clpfd 0.03 sec, 736,792 bytes true. ?- X #> X. false. I think there's an additional problem as well, corresponding to Henkin sentences—programs for which models do exist, but for which there is no unique minimal model. For example, we could try to formalize George W. Bush's foreign policy: withUs(You) :- person(You), \+ withTheTerrorists(You). withTheTerrorists(You) :- person(You), \+ withUs(You). person(chirac). Now we have two minimal models, one in which person(chirac), withUs(chirac) and one in which person(chirac), withTheTerrorists(chirac). (Thus we can explain Freedom Fries, one of the most ridiculous and terrifying aspects of the politics of the early 02000s.) Further inference rules might rule out one, the other, or both of these models. In the same way, the stratification rule rejects this program: withUs/1 needs to be above (evaluated later than) withTheTerrorists/1, but also vice versa. I'm not sure how to state this so SWIPL's CLP(FD) can tell that it's unsolvable, but that's probably because I'm a total noob at logic in general: ?- X #> Y, Y #> X. X#=<Y+ -1, Y#=<X+ -1. ?- X #> Y, Y #> X, label([X, Y]). ERROR: Arguments are not sufficiently instantiated Of course it is not a hard problem to assign strata—a straightforward topological sort will immediately reject the loop. The stratification rule is conservative, though; not only will it reject all the undecidable problems, it will also reject some programs where a unique minimal model does exist; as a trivial example: withUs(chirac). withUs(You) :- person(You), \+ withTheTerrorists(You). withTheTerrorists(You) :- person(You), \+ withUs(You). person(chirac). So it makes sense that people would look for looser restrictions that still guarantee decidability. Anyway, that's my understanding of the situation! I might be mistaken about basic things. Thanks for the reference to the book! It looks great and I'll try to read it. Or, I guess, work through it.

namibj 6y ago

The notably limitation being that you can't combine negation and recursion.

YeGoblynQueenne 6y ago
Thanks, I think that's the main intuition to draw from this. But I figured OP (kragen) wanted to understand the why, also.
- kragen 6y ago
  Indeed!