Why does this implementation of sorto does not terminate?

Question

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

Honestly, I think you need to narrow the scope of the question with less code needing to be reviewed. — Pumphouse
– Pumphouse, Commented Nov 8, 2017 at 22:39

cgrand · Accepted Answer · 2017-11-10 20:45:23Z

1

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

answered Nov 10, 2017 at 20:45

cgrand

7,95930 silver badges32 bronze badges

Sign up to request clarification or add additional context in comments.

1 Comment

szymanowski Over a year ago

Thank you for the advices, I will take a closer look at this

Collectives™ on Stack Overflow

Why does this implementation of sorto does not terminate?

1 Answer 1

1 Comment

Your Answer

Hot Network Questions

Collectives™ on Stack Overflow

1 Answer 1

1 Comment

Your Answer

Sign up or log in

Post as a guest

Related