4 ms·

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

by 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. ^^'

YeGoblynQueenne 7y ago
Thanks for the papers you suggest! I'll try and have a quick look. I'm actually interested in the subject because my research does touch on Datalog (exactly because of the decidability guarantees). Agreed about the definitions of decidability and formal correctness. Agreed also about the expressivity of the pure subset of Prolog. Oh, I remember now about Datalog and deciding equality. Yes. Well. You hit these kinds of walls anytime you try to do anything intersting with logic above the propositional level. The history of logic programming is a history of one negative result after the other and the compromises that must be made to avoid them. C'est la vie. But we persist because there is a pot of gold at the end of the rainbow and what best way is there to spend your life than chasing rainbows? :0 >> 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. Yes, I agree absolutely about that. For example, my code doesn't _need_ the impure constructs. But it's a lot more efficient with them. So it's a trade-off. And a trade-off very common in Prolog which, to my opinion makes many pragmatic choices that sacrifice purity for the benefit of having a useable language. That goes for reasoning about correctnes, also. The fact that you can sometimes reason about program correctness, given you can accept some restrictions to what kind of programs you can reason about is already miles ahead from what is possible with anything that isn't a logic programming language. That has to count for something. >> 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. ^^' Aw, I enjoy writing Prolog. So much so that I left my lucrative career in the industry to do research that would let me write a lot of it :)

by j-pb 7y ago

YeGoblynQueenne 7y ago

Thanks for the papers you suggest! I'll try and have a quick look. I'm actually interested in the subject because my research does touch on Datalog (exactly because of the decidability guarantees). Agreed about the definitions of decidability and formal correctness. Agreed also about the expressivity of the pure subset of Prolog. Oh, I remember now about Datalog and deciding equality. Yes. Well. You hit these kinds of walls anytime you try to do anything intersting with logic above the propositional level. The history of logic programming is a history of one negative result after the other and the compromises that must be made to avoid them. C'est la vie. But we persist because there is a pot of gold at the end of the rainbow and what best way is there to spend your life than chasing rainbows? :0 >> 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. Yes, I agree absolutely about that. For example, my code doesn't _need_ the impure constructs. But it's a lot more efficient with them. So it's a trade-off. And a trade-off very common in Prolog which, to my opinion makes many pragmatic choices that sacrifice purity for the benefit of having a useable language. That goes for reasoning about correctnes, also. The fact that you can sometimes reason about program correctness, given you can accept some restrictions to what kind of programs you can reason about is already miles ahead from what is possible with anything that isn't a logic programming language. That has to count for something. >> 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. ^^' Aw, I enjoy writing Prolog. So much so that I left my lucrative career in the industry to do research that would let me write a lot of it :)