Understanding core.logic !=

Question

I would expect the following expression to return a number of results, each of which consists of two cons cells, where the two cons cells are not equivalent. However, it returns 0 results. Why am I getting no results?

(run* [c1 c2] 
  (fresh [lx ly x1 y1 x2 y2] 
    (== lx [1 2])
    (== ly [4 5])
    (membero x1 lx)
    (membero x2 lx) 
    (membero y1 ly)
    (membero y2 ly)
    (conso x1 y1 c1)
    (conso x2 y2 c2)
    (!= c1 c2)))

Examples of expected results:

[(1 . 4) (2 . 5)]
[(1 . 4) (1 . 5)]
[(2 . 4) (2 . 5)]

I would not expect it to return a result like [(1 . 4) (1 . 4)] where both spots in each cons are equal.

If I remove the (!= c1 c2) portion, I get 16 results, including those where both cons are the same.

I get the results I expect if I replace (!= c1 c2) with:

(conde
  ((!= x1 x2))
  ((!= y1 y2)))

which should do the same thing, but explicitly checks the two cells.

Why does the first expression have results, but the second one doesn't, even though the only differences are seemingly equivalent? — Brigham
Ooops conde, membero, and all that are part of Clojure core logic. I'll have to look those up. — octopusgrabbus
Those functions are part of clojure/core.logic. The source is available on Github. — Brigham

dnolen dnolen · Accepted Answer · 2013-05-10T16:12:22

This is not a valid core.logic program. You cannot use conso where the tail is not proper. miniKanren in Scheme will let you do this, but the behavior is undefined for core.logic. I've amended the docstring for conso to reflect this. A working program:

(run* [c1 c2] 
  (fresh [lx ly x1 y1 x2 y2] 
    (== lx [1 2])
    (== ly [4 5])
    (membero x1 lx)
    (membero x2 lx) 
    (membero y1 ly)
    (membero y2 ly)
    (== [x1 y1] c1)
    (== [x2 y2] c2)
    (!= c1 c2)))

Understanding core.logic !=

2 Answers