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

I think you're after this program: <div class="snippet-clipboard-content notransla

Disequality constraint not being honored about faster-minikanren HOT 3 CLOSED

michaelballantyne commented on July 29, 2024

Disequality constraint not being honored

from faster-minikanren.

Comments (3)

michaelballantyne commented on July 29, 2024

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.

from faster-minikanren.

Reilithion commented on July 29, 2024

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?

from faster-minikanren.

michaelballantyne commented on July 29, 2024

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 ***@***.***> 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 <#6 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/ABXPU2HgBOy6BD4jvH0OMK4ax-8uWHKWks5tTLvkgaJpZM4SAin3> .

from faster-minikanren.

Disequality constraint not being honored about faster-minikanren HOT 3 CLOSED

Comments (3)

Related Issues (13)

Recommend Projects

React

Vue.js

Typescript

TensorFlow

Django

Laravel

D3

Recommend Topics

javascript

web

server

Machine learning

Visualization

Game

Recommend Org

Facebook

Microsoft

Google

Alibaba

D3

Tencent