zlacker

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+(OP)
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+(OP)
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+9m
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+mp
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+Iq
> 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).