[Haskell-cafe] A better, fair, and terminating backtracking monad [Was: Concurrency question]

[oleg at pobox.com]

Dmitry Vyal wrote:
> Currently I'm playing with theorem-proving using resolution. So I need
> some technique to break a computation, if takes too long.

When it comes to resolution proofs, perhaps a better approach is
to use a better monad that natively offers termination guarantees. For
example, 

	http://pobox.com/~oleg/ftp/Computation/monads.html#fair-bt-stream

First of all, the monad can let succeed the computations that surely
diverge in List and similar monads. As the code at the end of that
file shows, the monad avoids depth-first traps, and can even handle
left-recursion at the monadic level. Furthermore, the monad has the
inherent `timing' metric: Incomplete eliminations. Each elimination is
bounded in time. One can specify the upper bound on the number of
eliminations and thus force the termination if no solution was found
thus far. It is possible to modify the run function of the monad to
return the continuation once the counter has expired. So, one can run
the monad for a bit more, if desired. In contrast to iterative
deepening, running the continuation does _not_ repeat any of the
previous work.

We have used the FBackTrack monad to implement a Datalog-like system
(with top-down. resolution-based search however), and we could
successfully solve the problem of finding the transitive closure in a
_cyclic_ graph (the poster problem for post-Prolog systems like
XSB). No tabling was needed. A scheme version of the monad was used in
a leanTAP theorem prover (for the full first-order predicate logic):

http://cvs.sourceforge.net/viewcvs.py/kanren/kanren/mini/leanTAP.scm
http://cvs.sourceforge.net/viewcvs.py/kanren/kanren/mini/book-si.scm

The original leanTAP prover was meant to be used with iterative
deepening. Our implementation removes the limiting counter from the
leanTAP (which throttles instantiations of a universally quantified
formula); the monad has enough strength to find the solution anyway
(Pelletier problems 43 and 38).