zlacker

Incidentally, SQL's recursive queries completely solve the cycle problem by essentially keeping track of the results as a database, which then allows it to prune search results that have already been seen. That's what you get when using UNION in a recursive query, but don't use UNION ALL, as that turns off that pruning effect. This is elegant, but not online.

That's the problem with breadth-first search though: how to make it online?

Conversely, that's the advantage of DFS: it's online because the only state it needs is a search path, and the search path is O(log N), which is small enough to consider online.

>>crypto+(OP)
My SQL is rusty after years of misuse, but what you describe is similar to tabled Prolog. "Tabling" or SLG-Resolution, basically uses memoization to avoid having to re-derive parts of a proof tree that have already been traversed (that's useful because in a proof tree there are often many identical sub-trees under different branches). It also switches the execution strategy from DFS to BFS and delays the execution of goals until they can be proved. That way it avoids infinite left-recursions.

But there's no way to always ensure termination unless one restricts expressivity. Right? Halting problem and all that. Recursion, like iteration, must always risk going infinite, else it is not complete.

The tradeoff between DFS and BFS is like you say and as the article above points out that's the reason DFS was chosen as the original execution strategy for Prolog. Tabling on the other hand can be very memory-hungry (in my applications I often run out of tabling space on my 64GB RAM laptop). In the end, with languages like Prolog, it's the old joke: "sound, complete, efficient- choose two".

>>YeGobl+n61
Thanks for confirming this. With your reply in mind I think there is no reasonable way to make BFS the default for a logic language, and the programmer will just have to choose between BFS and DFS.

In other words, the answer to TFA's title question is, I think, "no" as to backtracking/DFS.

>>YeGobl+n61
In SQL you say something like:

  WITH RECURSIVE transitive_closure AS (
      SELECT parent, child FROM things
    UNION
      SELECT tc.parent, t.child
      FROM things t
      JOIN transitive_closure tc ON tc.child = t.parent
  )
  SELECT * FROM transitive_closure;

where `transitive_closure` is a table that gets all the results of the computation. The engine will run the second part of the query repeatedly until no new rows are added to the `transitive_closure` table. (If you change `UNION` to `UNION ALL` and there's circular paths then this will not terminate.)

Sounds a lot like whatever "tabling" is in Prolog.

>>crypto+ws1
To be honest I'd like it to be possible to completely do away with graph search in Resolution-based theorem proving. Resolution itself assumes no search, it's only an inference rule that removes contradictions from a theory. The original paper on Resolution proposes various ways to implement it but they all come down to search of some sort. I guess that's all we know how to do in AI: search :/

>>crypto+Jv1
Likely. It depends on how the transitive_closure results are computed. In tabling it's still by resolution so you can still get stuck in infinite loops, e.g. on infinite right-recursions. I think maybe that's more similar to UNION ALL?

I should probably read a bit about this again. I rarely used recursive queries in SQL when I worked with it, not least because a couple of times I did, I got into trouble because they went haywire :)

>>YeGobl+5x1
> In tabling it's still by resolution so you can still get stuck in infinite loops, e.g. on infinite right-recursions. I think maybe that's more similar to UNION ALL?

Must be. With UNION you can't end up with an infinite loop unless you have infinite data (or you're implementing a table-valued Ackermann function and so you have... not infinite results but for all practical intents, yeah).