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))))) ``` On Thursday, August 12, 2021 at 7:26:54 AM UTC-4 [email protected] wrote: > 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. > -- You received this message because you are subscribed to the Google Groups "minikanren" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/minikanren/b5f8e13a-4e1e-4892-8a45-eb5e4311d0aen%40googlegroups.com.
