[YeGoblynQueenne]

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

[robsimmons]

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?)

[YeGoblynQueenne]

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