|
|
|
|
|
|
by falsissime
1213 days ago
|
|
|
> but the burning problem that datalog does fix is Prolog's semi-decidability, or in other words, its tendency to enter infinite recursions. Prolog's built-in search is not semidecidable.
https://en.wikipedia.org/wiki/Decidability_(logic)#Semidecid... As you observe, Prolog gets stuck in left-recursions. But iterative deepening for Prolog is semidecidable (among other fair methods). This indeed is restricted to the pure, monotonic subset of (full) Prolog together with all pure, monotonic extensions. |
|
|
Thanks, yes, I might be fudging terminology a bit.
Generally, when I talk about Prolog I mean definite programs (sets of definite clauses and Horn goals, the latter usually called "definite goals") under SLD-resolution. That's more or less what is usually meant by "pure" Prolog: definite programs, without not/1 implementing Negation-As-Failure, without the cut, and without side effects; and executed by giving an initial Horn goal as a "query". Entailment between definite clauses and satisfiability of definite programs is undecidable.
By "semi-decidable" I mean that an SLD-refutation proof will terminate if there is a branch of the proof that ends in □ and is of finite length. If such a branch does not exist, a proof will "loop" forever. That's regardless of whether the branch succeeds or fails, which is a bit of a fudge, but, in practice, there is no other way to decide the success or failure of a proof than to search all its branches.
Left-recursion is one way in which Prolog, with depth-first search, generates branches of infinite length, but you can get those with right-recursion also. There are restrictions of Prolog, like SLG-resolution (similar to DFS with iterative deepening) that don't loop on left-recursions but the general case remains undecidable.
Fortunately, there seem to be at least as many finite proofs as there are infinite ones, or in any case I have never encountered a Prolog program that looped inintially and that couldn't be rewritten to terminate, at least when called in the way it was meant to be called. And that's also a bit of a fudge.