A possible bug about disequality constraints in faster-miniKanren

[Dmitrii Kosarev]

Hey, folks

I'm studying faster-miniKanren and it seems that I found a program where the result answer seems to be wrong. It is probably related to the occurs check in the constraints implementation... Can you  look, please?

Happy hacking,
Dmitrii

(display
  (run* (q)
    (fresh (x y)
      (== q `(,x ,y))
      (=/= x y)
      (=/= y x)
    )))

; (((_.0 _.1) (=/= ((_.0 _.1)))))

[William Byrd]

Hi Dmitrii!

I believe that this is the correct, simplified answer. What answer
did you expect?

Cheers,

--Will

> --
> 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 minikanren+...@googlegroups.com.
> To post to this group, send email to minik...@googlegroups.com.
> Visit this group at https://groups.google.com/group/minikanren.
> For more options, visit https://groups.google.com/d/optout.

[Kakadu]

I think that all answers like `X such that X is not equal X` should be
considered wrong.

> You received this message because you are subscribed to a topic in the Google Groups "minikanren" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/minikanren/7DSQF1A9w3w/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to minikanren+...@googlegroups.com.

[Jason Hemann]

> I think that all answers like `X such that X is not equal X` should be
> considered wrong.

I too believe implementations of miniKanren should have that behavior. 

> (run 1 (q) (=/= q q))

() 

I think I understand this program to be doing something different. This is closer I would say to an answer like X and Y such that X is not equal to Y. 

> (run* (q)
    (fresh (x y)
      (== q `(,x ,y))

      (=/= x y)))

Am I misinterpreting your comment/suggestion?

JBH

>> email to minikanren+unsubscribe@googlegroups.com.

>> To post to this group, send email to minik...@googlegroups.com.
>> Visit this group at https://groups.google.com/group/minikanren.
>> For more options, visit https://groups.google.com/d/optout.
>
> --

> You received this message because you are subscribed to a topic in the Google Groups "minikanren" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/minikanren/7DSQF1A9w3w/unsubscribe.

> To unsubscribe from this group and all its topics, send an email to minikanren+unsubscribe@googlegroups.com.

> To post to this group, send email to minik...@googlegroups.com.
> Visit this group at https://groups.google.com/group/minikanren.
> For more options, visit https://groups.google.com/d/optout.

--

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 minikanren+unsubscribe@googlegroups.com.

To post to this group, send email to minik...@googlegroups.com.
Visit this group at https://groups.google.com/group/minikanren.
For more options, visit https://groups.google.com/d/optout.

--

JBH

[William Byrd]

Yes, this is the current behavior:

Chez Scheme Version 9.4.1
Copyright 1984-2016 Cisco Systems, Inc.

> (load "mk-vicare.scm")
> (load "mk.scm")

> (run* (q)
(fresh (x y)
(== q `(,x ,y))
(=/= x y)
(=/= y x)
))

(((_.0 _.1) (=/= ((_.0 _.1)))))

> (run 1 (q) (=/= q q))
()

> (run* (q)
(fresh (x y)
(== q `(,x ,y))
(=/= x y)

))

(((_.0 _.1) (=/= ((_.0 _.1)))))

Which seems consistent to me, since in (== q `(,x ,y)), x and y may
have different values.

>> >> email to minikanren+...@googlegroups.com.

>> >> To post to this group, send email to minik...@googlegroups.com.
>> >> Visit this group at https://groups.google.com/group/minikanren.
>> >> For more options, visit https://groups.google.com/d/optout.
>> >
>> > --
>> > You received this message because you are subscribed to a topic in the
>> > Google Groups "minikanren" group.
>> > To unsubscribe from this topic, visit
>> > https://groups.google.com/d/topic/minikanren/7DSQF1A9w3w/unsubscribe.
>> > To unsubscribe from this group and all its topics, send an email to

>> > minikanren+...@googlegroups.com.

>> > To post to this group, send email to minik...@googlegroups.com.
>> > Visit this group at https://groups.google.com/group/minikanren.
>> > For more options, visit https://groups.google.com/d/optout.
>>
>> --
>> 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 minikanren+...@googlegroups.com.

>> To post to this group, send email to minik...@googlegroups.com.
>> Visit this group at https://groups.google.com/group/minikanren.
>> For more options, visit https://groups.google.com/d/optout.
>
>
>
>
> --
> JBH
>

> --
> 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 minikanren+...@googlegroups.com.

[Kakadu]

It seems that I misunderstood this stuff because in ocanren we print
disequality constraints in the result term: near free logical
variables. So, I parsed the answer as q = (_.0 _.1) when q =/= (_.0
_.1)

Question closed.

[William Byrd]

I highly recommend testing OCanren on these disequality tests:

https://github.com/webyrd/miniKanren-with-symbolic-constraints/blob/master/disequality-tests.scm

Some of the tests are quite subtle, and they ensure that the reified
answers reove duplicate and subsumed and irrelevant constraints.