why does the output of core.logic give the same value repeated?

Question

I tried this in core.logic

(require [clojure.core.logic :as l])

(l/run* [q]
  (l/fresh [a b c]
    (l/membero a [1])
    (l/membero b [4 5])
    (l/membero c [1 2])
    (l/== q [a b])))

expecting the result to be [1 4] [1 5]

but it was [1 4] [1 4] [1 5] [1 5]

then I started playing with it and found this:

(require [clojure.core.logic :as l])

(l/run* [q]
  (l/fresh [a b c]
    (l/membero a [1])
    (l/membero b [4 5])
    (l/membero c [1 1 1 1 1 1 1 1])
    (l/== q [a b])))

 ;; => ([1 4] [1 4] [1 4] [1 5] [1 4] [1 4] [1 5] [1 4] [1 5] [1 4] [1 5] [1 5] [1 5] [1 5])

where there is a [1 5] interspersed with [1 4]

what is happening? is this repetition thing supposed to be a feature or a bug?

Answer 1

This is because the usage of the logic variable c which is not required as it is not being unified with q. If you remove c then you will get desired result. Basically you need to understand how the substitution works in core.logic to understand why you are getting these duplicate results because of c.

At a high level the process is like searching a tree for solutions, in this case each element in the vector which is membero with c leads to a node in the search tree and that causes duplicate results because for each node introduced by c probable values leads to correct result as c isn't used in the unification (l/== q [a b])