miniKanren with a pure negation operator

miniKanren is a logic programming language designed by Dan Friedman, William Byrd and Oleg Kiselyov.

While elegantly designed, miniKanren hasn't a "pure" negation operator. There is a 'conda' operator which is similar to Prolog's cut, but these operators are not pure. That means once they are used, we may miss possible answers even they exist.

Out of this motivation, I reimplemented miniKanren and added a negation operator in it. The negation operator is pure in the sense that it doesn't cut out possible answers if they exist.

How it works?

The principle behind this operator (named "noto") is to propagate the negation of goals as constraints down the execution of the miniKanren program.

1. When the negation of a goal G is first encountered (as (noto G), a specially designed "evil unifier" is invoked, whose only goal is to take every chance to make the goal G fail.

2. If the evil unifier failed to make G fail no matter how hard it tries, the currrent execution path is considered to fail. This is because G will definitely succeed, thus (noto G) is doomed to failure.

3. If the evil unifier successs in making G fail, then (noto G) has a chance to succeed. But at this moment it is too early to declare success, because there might be other values which the ungrounded logic variables may pick up later, which will make G succeed (and thus make (noto G) fail.

4. Because of (3), we have to propagate the negation of G as a constraint down the stream of the execution, checking that G fails, every time we have new information about the logic variable.

5. If at the end of the execution path, we still can make G fail, then we can declare success of (noto G), under the condition that none of the "free" logic variables can take values that can make G succeed.

6. A success together with the constraints on the logic variables will be output together to denote the goal.

Limitations

Nested negations will not work nicely, so if you have (noto (noto (== x 10))), you are not guaranteed to have x bound to 10. More work needs to be done to make nested negations work.

Example

The working of the negation operator (and related 'condc' operator) can be explained by the following "unreasonable" example from The Reasoned Schemer (Frame 30).

(run* (out)
 (fresh (y)
   (rembero1 y `(a b ,y d peas e) out)))

;; =>
;; (((b a d peas e) ())               ; y == a
;;  ((a b d peas e) ())               ; y == b
;;  ((a b d peas e) ())               ; y == y
;;  ((a b d peas e) ())               ; unreasonable beyond this point
;;  ((a b peas d e) ())
;;  ((a b e d peas) ())
;;  ((a b _.0 d peas e) ()))

In this example, we got 7 answers, 4 of which shouldn't happen, because the fresh variable y should never fail to remove itself and then go on to remove d, peas and e.

If we use the 'condc' operator to redefine remebero, we will have the following (more reasonable) results:

;; redefine rembero using condc operator
(define rembero
  (lambda (x l out)
    (condc
      ((nullo l) (== '() out))
      ((caro l x) (cdro l out))
      ((fresh (res)
         (fresh (d)
           (cdro l d)
           (rembero x d res))
         (fresh (a)
           (caro l a)
           (conso a res out)))))))


(run* (out)
 (fresh (y)
   (rembero y `(a b ,y d peas e) out)))


;; =>
;; (((b a d peas e) ())
;;  ((a b d peas e) ())
;;  ((a b d peas e)
;;   (constraints:
;;    ((noto (caro (b #1(y) d peas e) #1(y)))
;;     (noto (caro (a b #1(y) d peas e) #1(y)))))))

We got only 3 answers, plus two constraints for the third answer. The constraints are basically saying: If we are to have this answer, neither (caro (b y d peas e) y) nor (caro (a b y d peas e) y) should hold.