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