5 ms·

isn't backtracking a complete search strategy?

by cerved 2y ago

desdenova 2y ago
That phrase was badly written. Backtracking is a complete search of the problem-space. What is incomplete is the Horn-SAT problem space, which is a subset of SAT, that can be solved in polynomial time, and is what Prolog is based on. A complete logic system would have to solve SAT, which is NP-complete. At least that's what I understood they meant by that.
- YeGoblynQueenne 2y ago
  Yeah, it's confusing. The article is referring to the incompleteness of Prolog implemented using Depth First Search. That's what the author means by "backtracking". I know this because I know "backtracking" is used in the logic programming community to stand for DFS, but if you don't know the jargon you'd be right to be confused. You can kind of, er, glean, that meaning in the article if you see how they refer to a "fixed" search strategy, and also notice that "backtracking" is not normally a search strategy since it can't search on its own. "Backtracking" is really "DFS with backtracking". The article is pointing out that Prolog with backtracking DFS is incomplete with respect to the completeness of SLD-Resolution. To clarify, SLD-Resolution is complete for refutation, or with subsumption. Prolog is an implementation of SLD-Resolution using DFS with backtracking. DFS is incomplete in the sense that it gets stuck in infinite loops when an SLD tree (the structure searched by DFS in Prolog) has cycles, especially left-recursive cycles. The article gives an example of a program that loops forever when executed with DFS with backtracking, in ordinary Prolog. SLD-Resolution's completeness does not violate the Church-Turing thesis, so it's semi-decidable: SLD-trees may have infinite branches. To be honest I don't know about the equivalence with Horn-SAT, but Resolution, restricted to definite clauses, i.e. SLD-Resolution, is complete (by refutation and subsumption, as I say above, and respecting some structural constraints to do with the sharing of variables in heads and bodies of clauses). We got several different proofs of its completeness so I think we can trust it's true. Edit: where does this knowledge about Horn-Sat come from? Do you have references? Gimme gimme gimme.
usgroup 2y ago
Depth first search is not complete if branches can be infinitely deep. Therefore if you're in the wrong infinite branch the search will never finish. Breadth first search is complete even if the branches are infinitely deep. In the sense that, if there is a solution it will find it eventually.
- desdenova 2y ago
  In practice, though, with BFS you'd run out of memory instead of never finding a solution. Also, there shouldn't be many situations where you'd be able to produce infinite branches in a prolog program. Recursions must have a base case, just like in any other language.
  - YeGoblynQueenne 2y ago
    This has to do with the ordering of search: searching a proof tree (an SLD tree, in SLD-Resolution) with DFS, as in Prolog, can get stuck when there are cycles in the tree. That's especially the case with left-recursion. The article gives an example of a left-recursive program that loops if you execute it with Prolog, but note that it doesn't loop if you change the order of the clauses. This version of the program, taken from the article, loops (I mean it enters an infinite recursion): last([_H|T],E) :- last(T,E). last([E],E). ?- last_(Ls,3). % Loops This one doesn't: last([E],E). last([_H|T],E) :- last(T,E). Ls = [3] ; Ls = [_,3] ; Ls = [_,_,3] ; Ls = [_,_,_,3] ; Ls = [_,_,_,_,3] ; Ls = [_,_,_,_,_,3] . % And so on forever To save you some squinting, that's the same program with the base-case moved before the inductive case, so that execution "hits" the base case when it can terminate. That's half of what the article is kvetching about: that in Prolog, you have to take into account the execution strategy of logic programs and can't just reason about the logical consequences of a program, you also have to think of the imperative meaning of the program's structure. It's an old complain about Prolog, as old as Prolog itself.
    - agumonkey 2y ago
      IIRC Markus Triska showed a trick (with a nickname i forgot) to constrain the search space by embedded a variable length into the top level goal.

isn't backtracking a complete search strategy?

by cerved 2y ago

isn't backtracking a complete search strategy?

That phrase was badly written. Backtracking is a complete search of the problem-space. What is incomplete is the Horn-SAT problem space, which is a subset of SAT, that can be solved in polynomial time, and is what Prolog is based on. A complete logic system would have to solve SAT, which is NP-complete. At least that's what I understood they meant by that.

YeGoblynQueenne 2y ago
Yeah, it's confusing. The article is referring to the incompleteness of Prolog implemented using Depth First Search. That's what the author means by "backtracking". I know this because I know "backtracking" is used in the logic programming community to stand for DFS, but if you don't know the jargon you'd be right to be confused. You can kind of, er, glean, that meaning in the article if you see how they refer to a "fixed" search strategy, and also notice that "backtracking" is not normally a search strategy since it can't search on its own. "Backtracking" is really "DFS with backtracking". The article is pointing out that Prolog with backtracking DFS is incomplete with respect to the completeness of SLD-Resolution. To clarify, SLD-Resolution is complete for refutation, or with subsumption. Prolog is an implementation of SLD-Resolution using DFS with backtracking. DFS is incomplete in the sense that it gets stuck in infinite loops when an SLD tree (the structure searched by DFS in Prolog) has cycles, especially left-recursive cycles. The article gives an example of a program that loops forever when executed with DFS with backtracking, in ordinary Prolog. SLD-Resolution's completeness does not violate the Church-Turing thesis, so it's semi-decidable: SLD-trees may have infinite branches. To be honest I don't know about the equivalence with Horn-SAT, but Resolution, restricted to definite clauses, i.e. SLD-Resolution, is complete (by refutation and subsumption, as I say above, and respecting some structural constraints to do with the sharing of variables in heads and bodies of clauses). We got several different proofs of its completeness so I think we can trust it's true. Edit: where does this knowledge about Horn-Sat come from? Do you have references? Gimme gimme gimme.

usgroup 2y ago

Depth first search is not complete if branches can be infinitely deep. Therefore if you're in the wrong infinite branch the search will never finish. Breadth first search is complete even if the branches are infinitely deep. In the sense that, if there is a solution it will find it eventually.

desdenova 2y ago
In practice, though, with BFS you'd run out of memory instead of never finding a solution. Also, there shouldn't be many situations where you'd be able to produce infinite branches in a prolog program. Recursions must have a base case, just like in any other language.
- YeGoblynQueenne 2y ago
  This has to do with the ordering of search: searching a proof tree (an SLD tree, in SLD-Resolution) with DFS, as in Prolog, can get stuck when there are cycles in the tree. That's especially the case with left-recursion. The article gives an example of a left-recursive program that loops if you execute it with Prolog, but note that it doesn't loop if you change the order of the clauses. This version of the program, taken from the article, loops (I mean it enters an infinite recursion): last([_H|T],E) :- last(T,E). last([E],E). ?- last_(Ls,3). % Loops This one doesn't: last([E],E). last([_H|T],E) :- last(T,E). Ls = [3] ; Ls = [_,3] ; Ls = [_,_,3] ; Ls = [_,_,_,3] ; Ls = [_,_,_,_,3] ; Ls = [_,_,_,_,_,3] . % And so on forever To save you some squinting, that's the same program with the base-case moved before the inductive case, so that execution "hits" the base case when it can terminate. That's half of what the article is kvetching about: that in Prolog, you have to take into account the execution strategy of logic programs and can't just reason about the logical consequences of a program, you also have to think of the imperative meaning of the program's structure. It's an old complain about Prolog, as old as Prolog itself.
  - agumonkey 2y ago
    IIRC Markus Triska showed a trick (with a nickname i forgot) to constrain the search space by embedded a variable length into the top level goal.