Non-termination when query variable is on a specific position

Question

Consider this blog post where the author implements palindrome relation using reverso:

(defn reverso [l r]
  (conde
    [(== l ()) (== r ())]
    [(fresh [la ld ldr]
      (conso la ld l)
      (appendo ldr (list la) r)
      (reverso ld ldr))]))

When I run (run* [q] (reverso q [1 2 3])), the output is ([3 2 1]). However, when I run (run* [q] (reverso [1 2 3] q)), the program does not terminate. I am able to get the correct result by explicitly requesting one result via run 1.

When experimenting, I was able to implement the same function myself using defne:

(defne conjo2 [l a la]
       ([[] _ [a]])
       ([[c . bs] _ [c . cs]] (conjo2 bs a cs)))

(defne reverso [l r]
       ([[] []])
       ([[a . ls] _]
        (fresh [rs]
               (conjo2 rs a r)
               (reverso ls rs))))

but the same issue is present. However, if I change my custom conjo2 to core.logic/conjo, the position of the variable during non-termination changes.

• Why does the program not terminate for the general query with specific locations of the query variable?
• Why specifying run 1 succeeds, but as soon as run 2 the program does not terminate?

Answer 1

The problem is that when you give appendo a fresh variable on the left and a fresh variable for the result, it can produce arbitrarily many answers, none of which will lead to a solution for your overall reverso question. Witness the definition of appendo:

(defne appendo
  "A relation where x, y, and z are proper collections,
  such that z is x appended to y"
  [x y z]
  ([() _ y])
  ([[a . d] _ [a . r]] (appendo d y r)))

It terminates if the x argument is empty (succeeding with y as the result); otherwise, it assumes that both x and the result z are non-empty lists and calls itself recursively. This terminates if either x or z can be proven to have a finite length, or if an index they share has a different value in the two lists. You never impose either of those constraints, so it continues searching forever.

Let's step through the execution of a simpler query, (run 2 [q] (reverso [1] q)).

1. We test whether l and r are both empty
2. They're not, so we fresh up some variables and assert that (conso la ld [1])
   1. This succeeds, binding (== la 1) and (== ld []).
3. Next we assert that (appendo ldr [1] r).
   1. This succeeds via the first clause in appendo, binding (== ldr []) and (== r [1]).
4. We recurse into (reverso [] []), and check whether both arguments are empty.
   1. This succeeds, so we yield our first overall result: (== q [1]) (remember that at the outer level (== q r), so a solution for r is a solution for q).
   2. We've been asked for more results, so we keep searching, which means rejecting the clause that just succeeded to see if alternatives might yield additional successes.
      1. Rejecting 4.1 is a quick dead end: we have (== l []) at this point, so the conso fails.
      2. Now we backtrack to 3.1, the empty-list clause in (appendo ldr [1] r). Rejecting this puts us in the second clause, (appendo d [1] r1), binding (== ldr [a . d]) and (== r1 [a . r]).

You can see this will never lead anywhere: the lists we're looking through are longer than the list we're trying to reverse. But before it can fail, it will make another recursive call to reverso, which will make a call to appendo, which will lengthen the lists again and make a recursive call to reverso, and so on. This is a simlar problem to that described in Goal ordering in Clojure's `core.logic`.

You can fix this by first informing the engine that you expect the two lists to be the same length. Then attempts by appendo to lengthen its input and output beyond the limit will fail. First, define same-lengtho:

(defn same-lengtho [xs ys]
  (conde
   [(== xs ()) (== ys ())]
   [(fresh [x xs' y ys']
      (conso x xs' xs)
      (conso y ys' ys)
      (same-lengtho xs' ys'))]))

Then insert a call to same-lengtho before you start the main search¹:

(defn reverso* [l r]
  (conde
   [(== l ()) (== r ())]
   [(fresh [la ld ldr]
      (conso la ld l)
      (appendo ldr (list la) r)
      (reverso* ld ldr))]))

(defn reverso [l r]
  (all (same-lengtho l r)
       (reverso* l r)))

Defined as such, a run* query produces the correct results regardless of parameter order:

user=> (run* [q] (reverso q [1 2 3]))
((3 2 1))
user=> (run* [q] (reverso [1 2 3] q))
((3 2 1))

And just to show that we haven't accidentally done something one-directional with same-lengtho, observe that with totally fresh variables on both sides it still generates all possible lists and their reverses:

user=> (run 5 [a b] (reverso a b))
([() ()]
 [(_0) (_0)]
 [(_0 _1) (_1 _0)] 
 [(_0 _1 _2) (_2 _1 _0)] 
 [(_0 _1 _2 _3) (_3 _2 _1 _0)])

---

¹ You don't technically need both (== l ()) and (== r ()) anymore: either one will suffice since you pre-guaranteed that the lists are the same length. But to me it seems semantically nicer to leave in the redundant check.