4 ms·

Sure Datalog is a query language, but Prolog isn't. I object to datalog being viewed as a subset of prolog, other than for historical reasons. It's just not us

• YeGoblynQueenne 7y ago
  >> Edit: Some systems that arguably implement a superset of Datalog, but for which their Datalog subset is not a subset of Prolog are LogicBlox, Datomic, Datascript and TriQ-Lite. That's interesting, I didn't know about that. I might have a look now that you mention it. Regarding correctnes proofs, I think triska knows this subject better than me but my understanding has always been that if you stay within the pure subset of Prolog (i.e. no destructive update of terms, no reads and writes to the database and basically nothing with side-effects) then you can actually fully reason about your programs at least in principle. I see this in practice everytime I write an extensive piece of Prolog code (for the record, I do that a lot, for my PhD) and I end up using the assert/1-retract/1 mechanism to update the program database as the program runs. The problem with that is that it kicks you right out of the cozy world of immutability, right back to the world of programmig with mutable states. Once your program reaches a certain degree of complexity it becomes impossible to predict its state at any given point in time. [Edit: the reason is that if something goes wrong and your program fails unexpectedly, the program database is left in an unpredictable state - and you have to understand each such state with great precision or it all goes to hell in a handcart. You're back to doing memory allocation by hand basically]. The hurt I feel everytime I use the assert/retract mechanism, or rather, the difference between the level of pain using assert/retract compared to not using them, is, for me, a great measure of the extent to which pure Prolog code is predictable. I'd even say amenable to formal proofs of correcntess but I've never actually tried that, to be fair. As to decidability, my understanding is that you can either have Turing completeness, or decidability, but not both. So to slightly correct my comment from above, Datalog itself is decidable only given a finite constant and predicate signature (the set of constants and predicate symbols). But finiteness means incompleteness.
  • j-pb 7y ago
    Out of the examples I would take a look at the LogicBlox Stuff, they gave join algorithm research a big push with their Leapfrog-Triejoin. The following papers ascend in difficulty, and are based on each other, but offer a fascinating glimpse into the connection of DPLL SAT solving and Conjunctive Query evaluation. https://openproceedings.org/2014/conf/icdt/Veldhuizen14.pdf https://openproceedings.org/2014/conf/icdt/Veldhuizen14.pdf https://arxiv.org/abs/1310.3314 https://arxiv.org/abs/1310.3314 https://arxiv.org/abs/1404.0703 https://arxiv.org/abs/1404.0703 As for reasoning and decidability, I think we need to clarify the decidability we're talking about. Decision problems are decidable or undecidable, and when one talks about decidability for a logic one usually means the decision problem wether a given formula of the logic is valid or not. Everything finite is always decidable, because you can just enumerate all possibilities. And logics without negation (like Datalog without stratified negation) are generally (?) decidable because you can just construct a Herbrand interpretation accordingly. However when we talk about correctness and formal reasoning there are other decision problems which are relevant, most of them revolve around stuff like "does this program implement this specification?", "does this program terminate?", "is this program keeping these invariants?", "are these two programs equal?" Note that even if these problems are undecidable, it doesn't mean that they're always undecidable, just that they're not decidable in general, e.g. the halting problem is undecidable, but I can give you infinitely many turing-machines which always halt. The pure side effect free fragment you describe is still at least as (?) powerful as FOL, even HOL if you include the meta predicates like call, thanks to the build-in predicates like forall. Heck I guess the build-in arithmetic alone will cost you decidability (of validity). Datalog is even more restricted than what you describe and equality of two Datalog programs is not decidable according to https://core.ac.uk/download/pdf/82609701.pdf https://core.ac.uk/download/pdf/82609701.pdf So the question is, how much reasoning a.k.a. how many decision problems can you actually do/solve on Datalog and Prolog. For Datalog, I'd say quite a bit, but not everything, and for Prolog I'd argue very little. But both give you a lot of power in return and that's the price you have to pay. Edit: And yeah, I don't envy you, on having to work with side-effectful prolog code. At some point it's just writing C with extra steps, ground through the Warren Abstract Sausage Machine. ^^'
    • 7y ago