> > The evaluator of the logic
> > system is complete: if there is a solution, the evaluator
> > will always find it in finite time.
>
> Is it also terminating? So if there is no solution it will tell you so.
The evaluator used in the yesterday's message -- no. It is merely
complete; if no solution exists, it may terminate, but it is not
obliged to. It depends on the formulation of the problem.
We do have a refutationally complete evaluator, which does find a
contradiction if one exists. It easily handles the problems like (in
Prolog notation)
X = 1, repeat, X = 2
and more complex problems. It might work for the de-typechecker, I
haven't tried. Alas, it takes _too_ much time at present for problems I
really want it to use; those problems, in addition to large depth,
have a very large breadth...
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
