oleg@pobox.com wrote:
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.
Thanks a lot. I was seeking for some material about monads in order to understand them better. I've just became studying your article. It promises to be very useful to me. But it doesn't clear to me, why my first attempt failed. In "Control.Concurrent" it's said, that GHC implements preemptive multitasking when there are no tight loops without allocations, so my approach should be successful too. Then I'll start writing some practical programs, I'm sure I'll have to deal with concurrency. So it would be great if someone points on my mistakes or misunderstandings. Thanks in advance.