Unfortunately, starting from a perspective that logic programming is mostly Prolog is a pretty bad way of getting to understand what Dusa is about. There's nothing wrong with that starting point, it's just... kind of like trying to understand Kotlin because you learned Smalltalk and know that both are object-oriented.
The linked page suggests one intro if you have experience with Datalog, another intro if you have experience with Answer Set Programming (ASP), and a third for everyone else. That's because Datalog and ASP are the two logic programming things that are most like finite-choice logic programming. Finite-choice logic programming gives a completely new way of understanding what answer set programs mean. The Dusa implementation is able to solve some problems vastly more efficiently than state-of-the-art ASP solvers, and is able to easily solve other problems that mainstream ASP solvers are simply unable to handle because of something called the "grounding bottleneck." Right now it's not a strict win by any means: there are many problems that Dusa chokes on that state-of-the-art ASP solvers can easily handle, but we know how to solve at least some of those problems for implementations of finite-choice logic programming.
All implementations of Answer Set Programming I am aware of are actually Turing complete, as are many practical implementations of the Datalog idea, and so is Dusa — this is a common misconception!
From the paper: "often people take “Datalog” to specifically refer to “function-
free” logic programs where term constants have no arguments, a condition sufficient to ensure that every program has a finite model. We follow many theoretical developments and practical implementations of datalog in ignoring the function-free requirement." If every program has a finite model, the language cannot be Turing complete: the reverse is not necessarily true but in practice the reverse is usually true.
>> If every program has a finite model, the language cannot be Turing complete: the reverse is not necessarily true but in practice the reverse is usually true.
What is the reverse here? Sorry it's late and I can't calculate it.
Btw, what I know about ASP is that it is incomplete (in the sense of soundness and completeness). Turing completeness is a separate question.
If every program has a finite model, the language cannot be Turing complete.
If it is not possible to give every program a finite model, that doesn't imply that language IS Turing complete. However, in practice, a Datalog-family logic programming language where some programs have infinite models is likely, in my experience, to be Turing Complete.
(For what it's worth, I don't know what it means for ASP to be incomplete in the sense of soundness and completeness. Incomplete relative to what other thing?)
>> If it is not possible to give every program a finite model, that doesn't imply that language IS Turing complete. However, in practice, a Datalog-family logic programming language where some programs have infinite models is likely, in my experience, to be Turing Complete.
Thanks, yes, that makes sense. But I'm not convinced of arguments "in practice". In practice, why do we care about Turing completeness? It's not like anyone sells infinite tape. But "in practice" we end up having no idea what are the limits of this or that system, so some principled reasoning is sometimes useful... practically useful.
>> (For what it's worth, I don't know what it means for ASP to be incomplete in the sense of soundness and completeness. Incomplete relative to what other thing?)
Relative to proofs: a proof procedure is complete if, when there exists a proof of some formal statement, the procedure can always derive that proof. Consider Resolution; say A |= B; then there exists a Resolution-refutation of A ∧ ¬B (i.e. the derivation of the empty clause A ∪ ¬B ⊢ □) so Resolution is refutation-complete. As far as I understand it this is not the same as Turing completeness, which is about a system being able to compute every program a Universal Turing Machine can compute. E.g. the first order predicate calculus is Turing complete and its restriction to Horn clauses is also Turing complete, but that doesn't necessarily imply the existence of a complete proof procedure for Horn clauses- that has to be shown separately.
Or at least that's how I think about it. I might be dead wrong there so please correct me if you have a better understanding of this than me.
There are many useful things that are not turing complete and still considered programming.
Regular Excel formulas are always terminating and therefore not computationally complete.
SQL without recursive CTEs is always terminating and therefore not computationally complete.
Simply typed lambda calculus is always terminating and therefore not computationally complete.
It's not the same, but restriction to terminating subsets gives very nice guarantees for a lot of program properties that would otherwise be undecidable.
I don't have any problems with calling it programming even if it's not Turing complete. But I think it's nice to clarify, so I can understand where it is in the expressivity-landscape.
Maybe it's obvious for the intended audience, given the mention of Datalog? But I suspect a lot of compsci people know of Prolog, and know about SAT(and similar) solvers, but don't really know how e.g Datalog places.
The linked page suggests one intro if you have experience with Datalog, another intro if you have experience with Answer Set Programming (ASP), and a third for everyone else. That's because Datalog and ASP are the two logic programming things that are most like finite-choice logic programming. Finite-choice logic programming gives a completely new way of understanding what answer set programs mean. The Dusa implementation is able to solve some problems vastly more efficiently than state-of-the-art ASP solvers, and is able to easily solve other problems that mainstream ASP solvers are simply unable to handle because of something called the "grounding bottleneck." Right now it's not a strict win by any means: there are many problems that Dusa chokes on that state-of-the-art ASP solvers can easily handle, but we know how to solve at least some of those problems for implementations of finite-choice logic programming.