A Logic Programming library for Clojure. At its heart is an original implementation of miniKanren as described in William Byrd’s dissertation Relational Programming in miniKanren: Techniques, Applications, and Implementations. It’s also described in great detail in the The Reasoned Schemer. However, do note that the version that appears in The Reasoned Schemer is an earlier implementation and differs from the one on which this library is based.
Performance is a central concern of this project. Anything that makes it slower will probably not be adopted. Anything that makes it faster without overly complicating the implementation will be considered. As of v0.4 it can solve the classic Zebra puzzle in about the same amount of time as SWI-Prolog. It would be interesting to see if we can approach the speed of Aquarius or Mercury on standard Prolog benchmarks.
This library is under heavy development as I cover the ideas in Byrd’s thesis and other sources on logic programming. It currently only supports the Clojure 1.3.0 alphas.
This is not the first implementation of miniKanren in Clojure. Jim Duey’s version can be found here. His work on that got me interested in logic programming in the first place.
YourKit has has given me a free license for their profiler, greatly simplifying the profiling of Logos performance.
YourKit is kindly supporting open source projects with its full-featured Java Profiler. YourKit, LLC is the creator of innovative and intelligent tools for profiling Java and .NET applications. Take a look at YourKit’s leading software products:
I stayed pretty true to the ideas of the original implementation. There are however several key differences. Unification uses protocols in order leverage the full speed of the host. Clojure’s cons operator differs significantly from Scheme’s so I added the LConsSeq protocol. Sequences which end in a logic variables can be represented by using lcons
(lcons 'a (lvar 'b)) ; (a . <lvar:b>)
Logic variables are instances of LVar not vectors as they are in Scheme.
The goal and goal constructor portion has been written from scratch on top of the protocols and makes liberal use of lazy sequences to prevent stack overflow.
Currently the Substitutions deftype uses clojure.lang.PersistentHashMap internally. This may be replaced with something that provides better performance for triangular substitutions.
- Simplicity. Optimizations should not destroy the ideas behind the original design. Any person willing to take take the time to understand the original Scheme implementation should have little trouble understanding how Logos is put together.
- Performance. This implementation is faster than miniKanren under Racket and seems to be close to performnace of miniKanren recorded by the original designers when running under Chez Scheme.
- Emphasis on pure relational programming.
I will only take contributions from people who have submitted Clojure CAs.
(run* [q] (rest-o q [1 2])) ; [(_.0 1 2)]
(run 5 [x]
(exist [y]
(append-o (llist 'cake y) '(d t) x)))
;; [(cake _.0 d t)
;; (cake _.0 _.1 d t)
;; (cake _.0 _.1 _.2 d t)
;; (cake _.0 _.1 _.2 _.3 d t)
;; (cake _.0 _.1 _.2 _.3 _.4 d t)]
(defn likes [x y]
(cond-e
((== x 'john) (== y 'mary))
((== x 'mary) (== y 'john))))
(defn musician [x]
(cond-e
((== x 'john))
((== x 'bob))))
(run* [q]
(likes q 'mary)
(musician q)) ;; [john]
(run* [q]
(musician q)) ;; [john bob]
(run* [q]
(exist [x y]
(likes x y)
(== [x y] q))) ;; [[john mary] [mary john]]
(unifier' '(?x ?y ?z) '(1 2 ?y)) ; (1 2 _.0)
The above is quite slow since we have to walk the data structure and replace the logic var symbols. It’s more efficient to prep the expressions before hand if you’re going to be unifying the same expressions over and over again.
(let [[u w] (map prep ['(?x ?y) (1 2)])] (unifier u w))
- Avoid unification at all costs, analyze miniKanren programs for ground terms. Instead use map/filter when possible which are 10X faster.
- Compilation to pure optimized Clojure ?
- Compilation to byte-code ?
- Fork/join ?
The design of miniKanren currently suffers from the closed principle. Relations are primarily defined through functions and so they are hard to extend. It would be preferable for the syntax to be more “open”. Consider the following Prolog snippet:
parent(pam, bob). parent(tom, bob). parent(tom, liz). parent(bob, ann). parent(bob, pat). parent(pat, jim). female(pam). female(liz). female(pat). female(ann). male(tom). male(bob). male(jim). offspring(Y,X) :- parent(X, Y). mother(X,Y) :- parent(X,Y), female(X).
Currently this is very verbose in logos.minikanren. We’d prefer something more along the lines of:
(rel parent
'[pam bob]
'[tom bob]
'[tom liz])
(extend-rel parent
'[bob ann]
'[bob pat]
'[pat jim])
(rel female
'pam 'liz 'pat 'ann)
(rel male
'tom 'bob 'jim)
(rel offspring
(parent ?x ?y))
(rel mother
(parent ?x ?y)
(female ?y))
Note that this syntax would not suffer from the “closed” property.
- Dynamic binding – the lazy nature of logos.minikanren means that you have to be careful with the use of dynamic binding with your logic programs. See this and this for an overview of the issues. It’s important to use
solveorsolve*instead ofrunorrun*if you would like dynamic bindings to affect your logic program.
- Concepts, Technqiues, and Models of Computer Programming, Chapters 9 and 12
- Art of the Propagator
- Constraint Propagation – Models, Techniques, Implementation
- Relational Programming in miniKanren: Techniques, Applications, and Implementations
- The Reasoned Schemer
- Efficient representations for triangular substitutions: A comparison in miniKanren
- A pattern matcher for miniKanren, or, how to get into trouble with CPS macros
- Kanren
- Logical JVM: Implementing the miniKanren logic system in Scala
- minikanren-scala
- Purely Functional Data Strucutres
- Using Datalog with Binary Decision Diagrams for Program Analysis
- Memoing for Logic Programs
- Efficient bottom-up abstract interpretation of prolog by means of constraint solving over symbolic finite domains