Factorial in Clojure core.logic

Question

I would like to write factorial using core.logic. I found this prolog snippet

factorial(0, 1).
factorial(N, M):- N1 is N - 1, factorial (N1, M1), M is N*M1.

and tried to translate it to core.logic in the following way

(defne factorialo [n m]
  ([0 1])
  ([n m] (fresh [n1 m1]
            (== (- n 1) n1)
            (== (* n m1) m)
            (factorialo n1 m1))))

(run* [q]
  (factorialo 3 q))

which fails with the message

clojure.core.logic.LVar cannot be cast to java.lang.Number
  [Thrown class java.lang.ClassCastException]

What is the proper way of writing factorial in core.logic?

Answer 1

Arithmetic in Prolog normally means implicit projection - you are no longer working relationally with logic variables but with the actual values they are bound to. There's no good sugar for this yet in core.logic, you must make the projection explicit:

(defne factorialo [n m]
  ([0 1])
  ([n m]
     (fresh [n1 m1]
       (project [n]
         (== n1 (- n 1)))
       (factorialo n1 m1)
       (project [n m1]
         (== m (* n m1))))))

(run 1 [q]
  (factorialo 3 q))

In the core.logic 0.8.0 alphas there is support for Constraint Logic Programming over Finite Domains. This improves the arithmetic story for Prolog:

(defne factorialfd [n m]
  ([0 1])
  ([n m]
     (fresh [n1 m1]
       (infd n1 m1 (interval 0 Integer/MAX_VALUE))
       (+fd n1 1 n)
       (factorialfd n1 m1)
       (*fd n m1 m))))

(run 1 [q]
  (infd q (interval 0 Integer/MAX_VALUE))
  (factorialfd 3 q))

Notice that the domains of the variables must be made explicit, but we no longer need to bother with projection. However this work is very alpha status and what this solutions looks like in the future is subject to change.