Is it possible to construct a negation of a relation?

[zaoqi libre]

Consider the following relation

```

(define (membero x l)
  (conde
   ((caro l x))
   ((fresh (d) (cdro l d) (membero x d)))))

```
Is it possible to construct a negation of it in miniKanren?

My first idea is to swap conj and disj, `==` and `=/=`

First, I simplified this relation

```
(define (membero x l)
  (fresh (a d)
         (== l (cons a d))
         (conde
          ((== l a))
          ((membero x d)))))

```

Then I did the swapping

```
(define (not-membero x l)
  (fresh (a d)
         (conde
          ((=/= l (cons a d)))
          ((=/= l a) (not-membero x d)))))

```

But the second conde clause did not look right.

Later I found that `fresh` also needs to be changed, but miniKanren does not have a `forall`

My second idea is implement miniKanren itself in miniKanren, then `(runo (membero x l) '())`. Even if this idea works, the performance will suffer.

[Greg Rosenblatt]

Hi zaoqi,

Negation and self-implementation of miniKanren are interesting topics.

Coincidentally, this year's miniKanren workshop features some papers covering these topics:

https://icfp21.sigplan.org/home/minikanren-2021#event-overview

You also might be interested in Evgenii's paper from 2019:

http://minikanren.org/workshop/2019/minikanren19-final4.pdf

(By the way, the workshop takes place next week, August 26th, if you're interested in attending!)

For the specific example of `membero` and `not-membero`, you can manually implement the necessary negation without needing universal quantification if you still constrain the second argument to be a list.  Here's a possible implementation:

```

(define (membero x xs)       
  (fresh (a d)                        
    (== xs `(,a . ,d))                
    (conde

      ((==  x a))                
      ((=/= x a) (membero x d)))))
                                      
(define (not-membero x xs)   
  (conde

    ((== xs '()))                
    ((fresh (a d)                
        (== xs `(,a . ,d))        
        (=/= x a)                 
        (not-membero x d)))))     

```