Can logic programming be liberated from predicates and backtracking? [pdf]

There already is a pretty major effort around the prolog community to build everything as much as possible around pure, monotonic prolog, and to provide a means to support multiple search strategies depending on the best fit for the problem. CLP libraries are also pretty common and the go-to for representing algebraic expressions relationally and declaratively.

I wouldn't say that the logic or relational way of describing effects is a bad thing either. By design it allows for multiple return values (foo/1, foo/2, ...) you can build higher level predicates that return multiple resources, which is pretty common for many programs. It makes concatenative (compositional) style programming really straightforward, especially for more complex interweaving, which also ends up being quite common. Many prolog implementations also support shift/reset, so that you can easily build things like conditions and restarts, algebraic effects, and/or debugging facilities on top. Prolog is also homoiconic in a unique way compared to lisp, and it's quite nice because the pattern matching is so powerful. Prolog really is one of the best languages I ever learned, I wish it was more popular. I think prolog implementations need a better C FFI interop and a nicer library ecosystem. Trealla has a good C FFI.

I think logic programming is the future, and a lot of these problems with prolog are fixable. If it's not going to be prolog, it'll probably be something like kanren and datalog within a lisp like scheme or clojure(script).

This is a great resource for getting a good feel of prolog: https://www.youtube.com/@ThePowerOfProlog/videos

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.

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

The way you write imperative programs in Prolog by exploiting the search order, using cuts, etc. seems clever when you see it in school and do a few assignments for a comparative programming languages class (the only 3 credit CS course I took) but it is painfully awkward if you have to do very much of it.

[Note I'm sick and tired; literally. I may not be firing on all cylinders in the following.]

The article is fudging things with its use of "backtracking" as a stand-in for backtracking Depth First Search (DFS)- the latter is the search strategy that is "fixed" in Prolog. And it's not really fixed. Prolog programs can also be executed by "tabling" a.k.a. SLG-Resolution, which basically replaces DFS with Breadth-First Search modulo momoization. Tabling avoids an important source of "incompleteness" in Prolog, that of non-terminating left-recursions.

To clarify, that is what makes Prolog "incomplete": that executing Prolog programs by DFS makes Prolog loop infinitely when encountering some left-recursions. The article gives the example of a last/2 predicate:

  last([_H|T],E) :- last(T,E).
  last([E],E).

This does indeed loop. But this one doesn't:

  last([E],E).
  last([_H|T],E) :- last(T,E).

  ?- last_(Ls,3).
  Ls = [3] ;
  Ls = [_,3] ;
  Ls = [_,_,3] ;
  Ls = [_,_,_,3] ;
  Ls = [_,_,_,_,3] ;
  Ls = [_,_,_,_,_,3] .

And that's what the article is pointing out with the allusion to "a higher, declarative programming style which frees the programmer from thinking about low-level control details". With such a "higher declarative programming style" the programmer does not have to think about program structure or execution strategy and can write whatever, however, and still get results!

The problem with that argument, which is as old as Prolog and possibly even older than that, is that it's an argument from taste, or, indeed, "style", to use the article's terminology. More specifically, for every non-terminating Prolog program that can be written, we can most likely write a Prolog program that does terminate, and that is (success-set) equivalent to the non-terminating program, by keeping in mind the structure of the search space for proofs traversed by ordinary Prolog with DFS, or tabling. And possibly with a few cuts here and there (oh, the humanity!). The article is simply arguing that it is "more declarative" to not have to do that. But, why is "more declarative" better? It's style all the way down.

As to the second axis of the argument, the horror of predicates that do not neatly map to "many" real world problems that are better represented as functions, asking whether we can liberate logic programming from predicates is like asking whether we can liberate the First Order Predicate Calculus from predicates, or, equivalently, make ice cream without the ice or the cream. Sure we can. The question is again: why? I don't see a clear justification for that. In particular, setting implementation details aside (as the article does on this point) SLD-Resolution is already sound and refutation-complete, or complete with subsumption. That is the best that can ever be achieved, and the article doesn't seem to claim anything else (or the ghosts of Alonzo Church and Alan Turing would be very, very sad). So this, too, seems to be a matter of taste: functions are more stylish than predicates. M'kay.

In fact, if I may blaspheme a little, this is what Church did with his Lambda calculus: he turned everything into typed functions to extend First Order Logic (FOL) into a higher order. And in the process completely destroyed the simple elegance of FOL. Why?