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