I'm a beginner with logic programming.
I'm trying to implement a sorting relation like this:
(sorto [3 2 1][1 2 3]) -> #s
I'am using clojure and core.logic:
I don't understand why this can not terminate in most cases.
Any idea would be helpful, thank you.
(require '[clojure.core.logic :refer :all]
'[clojure.core.logic.fd :as fd])
First I define several little helpers:
A simple count relation: (counto [a b] 2) -> #s
(defne counto [list n]
([() 0])
([[fl . rl] _]
(fresh [nnxt]
(fd/- n 1 nnxt)
(counto rl nnxt))))
reduce and every? relational equivalents:
(defne reduceo [rel acc x y]
([_ _ () _] (== acc y))
([_ _ [fx . rx] _]
(fresh [nacc]
(rel acc fx nacc)
(reduceo rel nacc rx y))))
(defne everyo [g list]
([_ ()])
([_ [fl . rl]]
(g fl)
(everyo g rl)))
min relation: (mino 1 2 1) -> #s
(defn mino [x y z]
(conde
[(fd/<= x y) (== x z)]
[(fd/> x y) (== y z)]))
relation between a list and its minimum element: (mino* [1 2 3 0] 0) -> #s
(defne mino* [xs y]
([[fxs . rxs] _]
(reduceo mino fxs rxs y)))
The main relation: (sorto [2 3 1 4] [1 2 3 4]) -> #s
(defne sorto [x y]
([() ()])
([[fx . rx] [fy . ry]]
(fresh [x* c]
(counto rx c)
(counto ry c)
(mino* x fy)
(rembero fy x x*)
(sorto x* ry))))
The below runs doesn't terminate, I would like to understand why.
(run* [q]
(sorto q [1 2]))
; does not terminate
(run* [q]
(sorto [2 1] q))
; does not terminate
(run* [a b]
(everyo #(fd/in % (fd/interval 10)) a)
(everyo #(fd/in % (fd/interval 10)) b)
(sorto a b))
;neither
The high level answer is because conjunction are tried in order. Reordering them may sometimes make a program to terminate -- however in the general case there may not exist a "good" order.
Have a look at Chapter 5 in https://scholarworks.iu.edu/dspace/bitstream/handle/2022/8777/Byrd_indiana_0093A_10344.pdf