[Haskell] Djinn and the inverse of a typechecker

oleg at pobox.com oleg at pobox.com
Thu Dec 15 18:43:21 EST 2005

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

More information about the Haskell mailing list