A pure logic negation operator for miniKanren

Have you ever noticed that some examples from "The Reasoned Schemer" are not so reasonable? If so, you may want to read this post.

Motivation

miniKanren is an educational logic programming language designed by Dan Friedman, William Byrd and Oleg Kiselyov. For teaching logic programming, they also co-authored the book "The Reasoned Schemer (TRS)." As a person hugely benefitted from this book (and also every other book of the "little book" series), I highly recommend TRS to you.

While elegantly designed, miniKanren hasn't a "pure" negation operator. There is a 'conda' operator which is similar to Prolog's cut, but it is not pure. That means once it is used, we may miss possible answers even if they exist. Thus although the 'conda' operator exists, it is not recommended for serious use.

But now we have a problem, if we can't have a 'cond' operator with implicit negation of the conditions of the previous lines, we will have trouble interpreting the results from some code from "The Reasoned Schemer (TRS)". For example, on "Frame 30" of TRS, we have the following program, which invokes rembero, a "logic function" for deleting an item from a list.

The definition of rembero is (notice the 'conde' operator):

(define rembero
  (lambda (x l out)
    (conde
      ((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)))))))

If it is used this way:

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

Running it and we have the following 7 answers:

;; =>
;; ((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))

Have you ever been surprised that there are 7 answers? Is it really possible that y fails to remove itself, but goes beyond and removes 'd', 'peas' and 'e' (Answers 4, 5 and 6), or fails to remove all of them (Answer 7)? Have you noticed that only the the first 3 answers are reasonable, and the last 4 answers shouldn't really happen?

For this particular example, the result from "The Reasoned Schemer" was not so reasonable.

a pure negation operator

As a student in Dan's class (B521), I was puzzled by the above results. I asked Dan and Will why this happens. They told me that this is because 'conde' operator of miniKanren is not exactly like 'cond' of Scheme. In Scheme, every line in the 'cond' expression implicitly negates all the previous conditions. This is to say, we execute the second line only if the first condition fails, and we execute the third line only if the conditions on the first and second lines both fail, and so on.

On the other hand, the 'conde' operator of miniKanren doesn't implicitly insert the negation of the conditions on the previous lines. The reason that miniKanren doesn't do this is because there is no easy way of doing "negation" in logic programming. According to Will Byrd, this is a thorny subject that has been researched for over 30 years.

As a dare devil who never believes how difficult things are, I thought: "Why not try my luck and see how far I can go competing with these 30 years of research?" Out of this evil-minded motivation, I independently reimplemented miniKanren and added a negation operator in it (named "noto", naturally). Different from 'conda' and Prolog's cut, noto is pure in the sense that it doesn't cut out possible answers if they exist. Using noto, I defined a new conditional construct named 'condc', which implicitly inserts negations of all previous conditions on each line. It is designed to behave as an exact logic counterpart of Scheme's 'cond'.

If we use the 'condc' operator to redefine remebero (only one character is changed), 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)))))))

Notice that we got only 3 answers (instead of 7), plus two constraints for the third answer. In fact each answer is paired with a constraint list, but the constraint lists are empty for the first two answers. This is why they are displayed as ((b a d peas e) ()) and ((a b d peas e) ()).

Now I briefly describe what these three answers mean. The first answer (b a d peas e) happens when "y is a", thus it removes the first item (a) from the list. The second answer (a b d peas e) happens when "y is b", thus it removes the second item (b) from the list. If you are confused why we still have a 'b' here after 'a', this is because the third item (y) is now 'b'!

The third answer is more interesting. It not only has an answer (a b d peas e), but also has two constraints attached to this answer:

(noto (caro (b #1(y) d peas e) #1(y)))
(noto (caro (a b #1(y) d peas e) #1(y)))

(Here #1(y) is a special notation to say that y is a logic variable.)

These constraints are in conjunctive form. They are 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, which is basically saying "y is neither a nor b". This is correct, because if y is either a or b, we would not have reached this answer because y would have removed one of the first two items, and the iteration would have stopped.

We have no more answers beyond the third, because under no condition should y be able to remove 'd', 'peas' or 'e', because the logic variable y will definitely remove y, no matter what it is! The iteration will definitely stop at the point where "y meets y". Clear?

How does it work?

The principle behind the negation operator ("noto") is to propagate the negation of goals as constraints (as in constraint logic programming) down the execution paths of the miniKanren program.

Before I tell you further details, I want to describe the intuition behind its design. Looking at the details without knowing the design principles will not be very useful. To see how you can design a negation operator, just think about how you can make the goal (noto G) succeed. First of all, you want to make the goal G fail, so that (noto G) can succeed, right? But G may contain unbound logic variables, and you can't just randomly assign them values. This is why a more elaborate mechanism was devised. It is there to ensure the soundness of the logic.

So now we can proceed to look at the details how this works:

1. When the negation of a goal G is first encountered, as (noto G), a specially designed "evil unifier" (unify-evil) is invoked. As its name suggests, unify-evil works similar to unify, but in a "negative way". The goal of unify-evil is to take every chance to make the goal G fail. Basically, it tries its best to find values that can be bound to the free logic variables, such that G can fail. But notice that unify-evil doesn't permanently associate those values to the logic variables. It just tries out those values, and as soon as it knows that G can fail, it dumps those associations. Thus the free logic variables remain free.
2. If unify-evil cannot make G fail no matter how hard it tries, then we know that G will succeed, thus we know that the goal (noto G) will fail. This means, we have failed to produce answers on this path. We should backtrack and explore other paths.
3. If unify-evil succeeds in making G fail, then (noto G) has a chance to succeed. But at this moment it is too early to declare success, because the unbound logic variables may pick up some other values later, which could make G succeed, and consequently make (noto G) fail.
4. Because of (3), we will have to propagate the negation of G as a constraint down the path of execution, checking that G fails every time when we have new information about the unbound logic variables (e.g. some fresh variables are later bound).
5. If at the end of the execution path unify-evil can still succeed in making G fail, then we can safely declare the success of (noto G). This is because the free logic variables will have no more chances to make G succeed. This (noto G), if it is not subsumed by the current substitution state, should be included in the final answer.
6. A reified value, together with the non-subsumed constraints on the logic variables, will be output together as the answer.

From the above mechanism, can you see why the example of rembero produces these results?

(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)))))))

Why hasn't the second answer a constraint which says "y is not a"? This is because for the second answer, we already know that "y is b", which implies "y is not a". The system is intelligent enough to omit "y is not a" from the answer's constraints because it knows that it is subsumed under the current substitution ("y is b").

Limitations

Nested negations does not work properly, so if you have (noto (noto (== x 10))), you are not guaranteed to have x bound to 10. I have a later version of the negation operator did make this work, but it caused non-termination problems, and I ran out of allocated time soon after that.  More work needs to be done to make nested negations work.

After several years of this experiment, I had an interesting discussion with Oleg Kiselyov on this topic. An excerpt of our conversation is included as comments at the bottom of the code. In his words, although the implementation of noto works to some degree, it is not perfect. To the best of his knowledge, no negation operators work perfectly until this day.

So, did I beat 30 years of hardcore research? Probably not. But consider this - it took me less than a month to think of and implement all this. I worked completely independently, day and night. This happened in 2008 when I first learned miniKanren and logic programming. Today as a mature programming languages researcher, I'd like to take it as an amusement to revisit and see how far I can go down the path I have started exploring 5 years ago.

Code

The reimplemented miniKanren, together with the negation operator, has been available from my GitHub for years without being noticed. Now I made it an independent project and hope to have time (and public pressure) to develop it further. I also hope to gather ideas from real logic programming gurus about other ways of implementing pure negation operators.

If you are interested in playing with it, or you want to research on this topic, my code is here for free:

http://github.com/yinwang0/ykanren