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.

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.

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

I'm not very sure about this either, I haven't used CLP(FD) much. triska, the OP in this thread, is the author of the CLP(FD) library and he could help but I guess he's probably moved on from this thread by now.

>> You're not letting us down! We're collaboratively exploring a fascinating space of promising ideas!

Thanks, that's a great kind of attitude to have. dang (always a champion of intellectual curiosity) will be proud of us :)

I did have a quick look through your comment and I think it's insightful and more correct than not, far as I can tell.

About this:

  epimenides :- \+ epimenides.

That is a contradiction and so does not have any model, as you say. While startification would indeed avoid this, deriving an empty model (or failing to derive a model) is correct behaviour because the formula is unsatisfiable. However (1) is a well-formed formula, certainly in First Order Logic, so it's not an invalid program, per se. In general contradictions and tautologies tend to be treated specially or ommitted from discussion, in logic programming theory often, I find, which makes sense because they're kind of obvious corner cases that nobody wants to spend too much time on. "p if not p" should always fail quickly.

Regarding minimal models, according to the book I linked, there are two datalogs with negation, datalog¬ (which does not allow recursion) and datalog¬¬ and they indeed eliminate the guarantee that a program has a unique minimal model under fixpoint semantics- so while a program is still guaranteed to have _a_ fixpoint that is reachable in finite time, this fixpoint is not guaranteed to be unique or minimal.

As to my sketch proof of undecidability, that would actually not work in pure datalog, where the deletion of facts is not allowed. Deletion of facts is allowed under datalog¬¬, whose syntax accepts rules with negated _heads_ that are interpeted as signifying a fact should be deleted. There are different options for the treatment of negated rule heads (e.g. deriving A and ¬A simultaneously can be interpreted as a contradiction that makes the program unsatisfiable) but now the guarantee of termination is lost because there is no guaranteed fixpoint. This is all from 14 of the Alice book and the example given is of a program that flip-flops between two models, much simpler than my three-atom case above, which I think after all is probably fictitious :)

>> 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.

I didn't know about Henkin sentences and I don't know how datalog (of any kind) semantics deal with them. An interesting lead for further reading, thanks.

Thank you! I'll be playing around with these ideas. BTW, I sent you an email, so we can correspond further when you aren't on a paper deadline :)

Thanks, yeah, I saw your email last night. Was too tired to reply. Well, please accept this a reply and thank you for getting in touch :)