4 ms·

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 f

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.
    - YeGoblynQueenne 2y ago
      I think what you mean is that he adds an argument that counts the times a goal is resolved with, thus limiting the depth of resolution? That works, but you need to give a magic number as a resolution depth limit, and if the number is too small then your program fails to find a proof that it normally should be able to find. It's not a perfect solution.
      - agumonkey 2y ago
        Yes, well not so much a constant value. He added an unbound variable and it was enough to alter the search. Indeed it's still more or a trick, but it got me interested if there were other more fundamental ideas beyond that.
        YeGoblynQueenne 2y ago
        That sounds like iterative deepening without a lower bound then. I guess that's possible. Maybe if you had a link to Markus' page I could have a look. There are techniques to constraint the search space for _programs_ rather than proofs, that I know from Inductive Logic Programming, like Bottom Clause construction in Inverse Entailment, or the total ordering of the Herbrand Base in Meta-Interpretive Learning (ILP). It would be interesting to consider applying them to constraint the space of proofs in ordinary logic progamming. Refs for the above techniques are here but they're a bit difficult to read if you don't have a good background in ILP: http://wp.doc.ic.ac.uk/arusso/wp-content/uploads/sites/47/2015/01/IE_PROGOL.pdf http://wp.doc.ic.ac.uk/arusso/wp-content/uploads/sites/47/20... https://link.springer.com/content/pdf/10.1007/s10994-014-5471-y.pdf https://link.springer.com/content/pdf/10.1007/s10994-014-547...
        agumonkey 2y ago
xelxebar 2y ago
Hrm. I guess the converse applies if nodes can have infinite children. That said, even if your tree is infinitely wide and deep, we're only dealing with countable children, right? Thus a complete traversal has to exist, right? For example, each node has unique path to root, so write <n1, n2, ..., nk> where each ni is the sibling ordinal of the node at depth i in that path, i.e. it's the ni-th sibling of the n(i-1)st node. Raising each of these to the ith prime and taking a product gives each node a unique integer label. Traverse nodes in label order and voilà? However, that all assumes we know the tree beforehand, which doesn't make sense for generic call trees. Do we just smash headfirst into Rice on this when trying to traverse in complete generality?
- usgroup 2y ago
  No breadth first search is still complete given an infinite branching factor (i.e. a node with infinite children). "Completeness" is not about finishing in finite time, it also applies to completing in infinite time. Breadth first search would visit every node breadth first, so given infinite time, the solution would eventually be visited. Meanwhile, say a branch had a cycle in it, even given infinite time, a naive depth first search would be trapped there, and the solution would never be found.
  - LegionMammal978 2y ago
    Suppose you have a node with two children A and B, each of which has infinitely many children. If you performed an ordinary BFS, you could get trapped in A's children forever, before ever reaching any of B's children. Or, suppose that a node has infinitely many children, but the first child has its own child. A BFS would get stuck going through all the first-level children and never reach the second-level child. A BFS-like approach could work for completeness, but you'd have to put lower-level children on the same footing as newly-discovered higher-level children. E.g., by breaking up each list of children into additional nodes so that it has branching factor 2 (and possibly infinite depth).
    - usgroup 2y ago
      Countable infinity does not work like that: two countable infinities are not more than one countable infinity. I think it falls into the "not even wrong" category of statements. The Wikipedia article is fairly useful: https://en.wikipedia.org/wiki/Countable_set https://en.wikipedia.org/wiki/Countable_set
agumonkey 2y ago
Reminds me that Warren made a talk about prolog term domains to study resolution over infinite branches.

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.
  - YeGoblynQueenne 2y ago
    I think what you mean is that he adds an argument that counts the times a goal is resolved with, thus limiting the depth of resolution? That works, but you need to give a magic number as a resolution depth limit, and if the number is too small then your program fails to find a proof that it normally should be able to find. It's not a perfect solution.
    - agumonkey 2y ago
      Yes, well not so much a constant value. He added an unbound variable and it was enough to alter the search. Indeed it's still more or a trick, but it got me interested if there were other more fundamental ideas beyond that.
      - YeGoblynQueenne 2y ago
        That sounds like iterative deepening without a lower bound then. I guess that's possible. Maybe if you had a link to Markus' page I could have a look. There are techniques to constraint the search space for _programs_ rather than proofs, that I know from Inductive Logic Programming, like Bottom Clause construction in Inverse Entailment, or the total ordering of the Herbrand Base in Meta-Interpretive Learning (ILP). It would be interesting to consider applying them to constraint the space of proofs in ordinary logic progamming. Refs for the above techniques are here but they're a bit difficult to read if you don't have a good background in ILP: http://wp.doc.ic.ac.uk/arusso/wp-content/uploads/sites/47/2015/01/IE_PROGOL.pdf http://wp.doc.ic.ac.uk/arusso/wp-content/uploads/sites/47/20... https://link.springer.com/content/pdf/10.1007/s10994-014-5471-y.pdf https://link.springer.com/content/pdf/10.1007/s10994-014-547...
        agumonkey 2y ago

xelxebar 2y ago

Hrm. I guess the converse applies if nodes can have infinite children. That said, even if your tree is infinitely wide and deep, we're only dealing with countable children, right? Thus a complete traversal has to exist, right? For example, each node has unique path to root, so write <n1, n2, ..., nk> where each ni is the sibling ordinal of the node at depth i in that path, i.e. it's the ni-th sibling of the n(i-1)st node. Raising each of these to the ith prime and taking a product gives each node a unique integer label. Traverse nodes in label order and voilà? However, that all assumes we know the tree beforehand, which doesn't make sense for generic call trees. Do we just smash headfirst into Rice on this when trying to traverse in complete generality?

usgroup 2y ago
No breadth first search is still complete given an infinite branching factor (i.e. a node with infinite children). "Completeness" is not about finishing in finite time, it also applies to completing in infinite time. Breadth first search would visit every node breadth first, so given infinite time, the solution would eventually be visited. Meanwhile, say a branch had a cycle in it, even given infinite time, a naive depth first search would be trapped there, and the solution would never be found.
- LegionMammal978 2y ago
  Suppose you have a node with two children A and B, each of which has infinitely many children. If you performed an ordinary BFS, you could get trapped in A's children forever, before ever reaching any of B's children. Or, suppose that a node has infinitely many children, but the first child has its own child. A BFS would get stuck going through all the first-level children and never reach the second-level child. A BFS-like approach could work for completeness, but you'd have to put lower-level children on the same footing as newly-discovered higher-level children. E.g., by breaking up each list of children into additional nodes so that it has branching factor 2 (and possibly infinite depth).
  - usgroup 2y ago
    Countable infinity does not work like that: two countable infinities are not more than one countable infinity. I think it falls into the "not even wrong" category of statements. The Wikipedia article is fairly useful: https://en.wikipedia.org/wiki/Countable_set https://en.wikipedia.org/wiki/Countable_set

agumonkey 2y ago

Reminds me that Warren made a talk about prolog term domains to study resolution over infinite branches.