search

michaelballantyne / faster-minikanren

A fast implementation of miniKanren with disequality and absento, compatible with Racket and Chez.
MIT License
154 stars 36 forks source link

Disequality constraint not being honored #6

Closed Reilithion closed 6 years ago

Reilithion commented 6 years ago

It looks like under certain circumstances the =/= constraint is not being honored:

> (run* (q r) (matche (q) (('A)) (('B))) (matche (q r) (('A 'a)) ((,?? 'b) (=/= q 'A))))
'(('A 'a) ('B 'b) ('A 'b))

In the second matche, I ask for r to be unified with 'b but I add the constraint that q not be equal to 'A. I expect there to only be two answers; q='A, r='a and q='B, r='b. But I get back a third answer, where q='A, r='b. I think this should have been forbidden by the disequality constraint.

Is this an actual issue with faster-minikanren or is it a problem with my understanding of the language?

michaelballantyne commented 6 years ago

I think you're after this program:

(run* (q r)                                                                                                                                                   
  (matche (q)                                                                                                                                                     
    ((A)) ((B)))                                                                                                                                    
  (matche (q r)                                                                                                                                                   
    ((A a))                                                                                                                                                 
    ((,?? b) (=/= q 'A))))

Notice the lack of quotes in the match patterns. Pattern positions are implicitly quoted; that's why you have to write the unquote in front of your pattern variable. Including a quote when not needed results in the data (quote A), say, instead of A. In contrast, the arguments to =/= are not implicitly quoted. So your first matche unifies q with the datum (quote A), whereas your disequality says q must not be the datum A.

Reilithion commented 6 years ago

Whoops. I noticed that a couple minutes ago and was about to modify my post. Actually, I got to that bad example while trying to minify a somewhat more elaborate one. Here:

> (run* (q r) (matche (q) (((X a))) (((Y b)))) (matche (q r) (((X ,??) a)) ((,?? b) (fresh (s) (=/= q `(X ,s))))))
'(((X a) a) ((Y b) b) ((X a) b))

The intent of the constraint in this one is that I don't want the value of q to be a list beginning with 'X. It doesn't seem to work. Is the only way I can do this to build it from conde and break down the cases?

michaelballantyne commented 6 years ago

Disequality constraints fail only when a unification of their arguments would succeed without extending the substitution. Stated another way, they fail when unification of their arguments would inevitably succeed. With the code you wrote, there are infinitely many values of s such that q is not (X ,s), so there's no reason for the constraint to fail.

I would think to express the constraint you describe as: (conde [(fresh (a d) (== q `(,a . ,d)) (=/= a 'X))] [(not-pairo q)])

Either it's a list but one that doesn't start with X, or not a list.

Unfortunately faster-miniKanren doesn't have not-pairo, though I know some other implementations do. Unless you feel like sorting through how to add that, I think the best you can do is enumerate things that aren't pairs that could be within your domain of discourse. Booleans, numbers, etc. We end up doing things like that in our relational pattern matcher implementation: https://github.com/michaelballantyne/faster-miniKanren/blob/master/full-interp.scm#L251

On Fri, Feb 9, 2018 at 4:43 PM Reilithion notifications@github.com wrote:

Whoops. I noticed that a couple minutes ago and was about to modify my post. Actually, I got to that bad example while trying to minify a somewhat more elaborate one. Here:

(run* (q r) (matche (q) (((X a))) (((Y b)))) (matche (q r) (((X ,??) a)) ((,?? b) (fresh (s) (=/= q `(X ,s)))))) '(((X a) a) ((Y b) b) ((X a) b))

The intent of the constraint in this one is that I don't want the value of q to be a list beginning with 'X. It doesn't seem to work. Is the only way I can do this to build it from conde and break down the cases?

— You are receiving this because you modified the open/close state.

Reply to this email directly, view it on GitHub https://github.com/michaelballantyne/faster-miniKanren/issues/6#issuecomment-364577334, or mute the thread https://github.com/notifications/unsubscribe-auth/ABXPU2HgBOy6BD4jvH0OMK4ax-8uWHKWks5tTLvkgaJpZM4SAin3 .