• 115 commits
• 4 branches
• 2 releases
• 1 contributor
• GPL-3.0

Reazon – miniKanren for Emacs

Reazon is an Emacs implementation of miniKanren, a small domain-specific logic programming language. Whereas languages like Elisp deal with functions that take inputs and yield outputs, miniKanren deals with sets of values that satisfy relations. Every function is a relation, but not vice versa, since a relation might include the output of a function but not its inputs. In such a case, miniKanren would attempt to find inputs yielding the output, effectively running the function backwards.

THAT’S VAGUE. HOW ABOUT AN EXAMPLE?

Great idea. Consider this recursive definition for the function append [fn:1]:

;; Use `_append' rather than `append' to avoid clobbering the builtin.
(defun _append (head tail)
  (let ((out
         (if (null head)
             tail
           (let* ((a (car head))
                  (d (cdr head))
                  (rec (_append d tail)))
             (cons a rec)))))
    out))

(list
 (_append '(1 2 3) '())
 (_append '() '(4 5 6))
 (_append '(1 2 3) '(4 5 6)))

((1 2 3)
 (4 5 6)
 (1 2 3 4 5 6))

In that definition, we set up a variable out and then assign it one of two values: tail if head is null, or else the cons of the car of head and the recursive appending of the cdr of head onto tail.

A miniKanren relation can be defined in the same way:

(reazon-defrel appendo (head tail out)
  (reazon-conde
   ((reazon-== head '()) (reazon-== out tail))
   ((reazon-fresh (a d rec)
      (reazon-== head (cons a d))
      (reazon-== out (cons a rec))
      (appendo d tail rec)))))

Again, we have variables head, tail, and out, and out is made to be tail when head is null and the cons of the car of head and the recursive appending of the cdr of head onto tail when it isn’t.

THEY LOOK LIKE THE SAME DEFINITION.

Indeed, appendo can be used just like append:

(let ((r1
       (reazon-run* out
         (appendo '(1 2 3) '() out)))
      (r2
       (reazon-run* out
         (appendo '() '(4 5 6) out)))
      (r3
       (reazon-run* out
         (appendo '(1 2 3) '(4 5 6) out))))
  (mapcar #'car (list r1 r2 r3)))

((1 2 3)
 (4 5 6)
 (1 2 3 4 5 6))

SO WHAT’S THE DIFFERENCE? AND WHY IS =out= AN INPUT?

A value can be supplied for out, in which case appropriate values will be found for head and tail:

(reazon-run* (head tail)
  (appendo head tail '(1 2 3 4 5 6)))

((nil
  (1 2 3 4 5 6))
 ((1)
  (2 3 4 5 6))
 ((1 2)
  (3 4 5 6))
 ((1 2 3)
  (4 5 6))
 ((1 2 3 4)
  (5 6))
 ((1 2 3 4 5)
  (6))
 ((1 2 3 4 5 6)
  nil))

SO THE INPUTS ARE OUTPUTS?

They can be. They can also be supplied along with the “output”, and they can even be supplied only partially:

(reazon-run* (head tail out)
  (reazon-fresh (a c d)
    (reazon-== head `(,a 2 ,c ,d)))
  (reazon-fresh (a b e)
    (reazon-== out `(,a ,b 3 4 ,e 6)))
  (appendo head tail out))

(((_0 2 3 4)
  (_1 6)
  (_0 2 3 4 _1 6)))

NOT BAD! BUT APPENDING LISTS TOGETHER ISN’T A VERY EXCITING APPLICATION.

Consider the function eval, commonly found in languages like Python and Javascript. It takes as input an expression and returns as output the value to which that expression evaluates. The relational equivalent of eval would be the relation evalo, which would associate expressions with values. Supposing we had such a relation, what be the result of the following query?

(reazon-run 1 q
  (evalo q q))

UHH…

Right, we would get a quine, that is, an expression that evaluates to itself! And supposing we had a disequality operator reazon-!= to stipulate that two expressions are distinct, what would we get from running this?

(reazon-run 1 (p q)
  (reazon-!= p q)
  (evalo p q)
  (evalo q p))

TWO DISTINCT EXPRESSIONS THAT EVALUATE TO EACH OTHER?

Yes, two twines!

WOW, REAZON CAN DO ALL THAT?

No. Currently Reazon lacks the ability to constrain values, or really to handle negation at all. I mean, the language is Turing-complete, so it’s certainly possible in some sense, but it can’t be done in a straightforward way.

Installation

For now, the best way to run Reazon is to open the file reazon.el and run the command eval-buffer. After that, all the Reazon functions, macros, and relations will be loaded up and you can start writing some queries!

IMPORTANT NOTE: Reazon relations must be defined in a context with lexical binding. To enable lexical binding, run (setq lexical-binding t) or put ;; -*- lexical-binding: t; -*- at the top of a source file. I’m serious, Reazon will not work without lexical binding.

Emacs Version

Because it relies on lexical binding, Reazon absolutely requires Emacs version 24+. It also uses the function gensym in its macros. This was added as a builtin function in Emacs 26, so running Reazon as-is requires at least that. However, gensym existed in other forms prior to 26, so Reazon can also be run in versions 24 and 25 by adding one of the following expressions:

(progn
  (require 'cl-lib)
  (defalias 'gensym 'cl-gensym))

or

(require 'cl)

FAQ

Did you come up with miniKanren all by yourself?

No. miniKanren is described in detail and implemented in the book The Reasoned Schemer (a sequel to The Little Schemer) by Byrd, Friedman, Kiselyov, and Hemann. Reazon is a straightforward adaptation to Elisp of the code from the second edition.

So you just copied some code out of a book?

To some extent, yes. The big differences between the code here and the code there are that 1) the macros are written with defmacro instead of define-syntax, and 2) certain control functions are written with explicit iteration instead of recursion, since Elisp lacks tail-call elimination.

How does this compare to Clojure’s core.logic?

core.logic is a Clojure implementation of miniKanren. It’s significantly more developed than Reazon (I mean, like way more developed), but they are the same in spirit. If you need to use miniKanren for something serious, use that, not this.

Why does “Reazon” have a “z” in it? That’s stupid.

Maybe. Initially it was just called “Reason” (with an “s”) after The Reasoned Schemer, but then I discovered to my dismay that there was already a package called “Reason” on Melpa (a major mode for some language). Changing the “s” to “z” seemed like a fine way around that roadblock, with the added benefit of making the name “pop”.

Why are all the relations named with o at the end (conso, listo, etc)? That’s ugly and weird.

I don’t know. That convention was established long before I came around miniKanren. In the context of Emacs, however, it actually fits in with another ugly convention, namely that of ending the names of test functions with p (consp, listp, etc). This suggests that, for example, conso is somehow similar to consp, which is accurate.

I ran a query, but I got *** Eval error *** Lisp nesting exceeds ‘max-lisp-eval-depth’.

The interface operator reazon-run* searches for as many solutions as it can find. If your query has infinitely many solutions, it will keep searching until it blows the stack. For instance, there are infinitely many triples x, y, z such that x and y append to form z, so the following query will error:

(reazon-run* (x y z)
  (appendo x y z))

Try using reazon-run (no asterisk) with a count to limit the search:

(reazon-run 3 (x y z)
  (appendo x y z))

((nil _0 _0)
 ((_0)
  _1
  (_0 . _1))
 ((_0 _1)
  _2
  (_0 _1 . _2)))

I defined a relation and ran a query, but I got *** Eval error *** Symbol’s value as variable is void: x. I double-checked and I’m sure I wrote the definition correctly.

Reazon relations need to be defined in lexical environments. This can be set in an interpreter like ielm by running (setq lexical-binding t) or by adding ;; -*- lexical-binding: t; -*- to the top of a source file.

I learned this the hard way.

In ielm:

> (reazon-defrel _five (x) (reazon-== x 5))
_five
> (reazon-run* q (_five q))
*** Eval error ***  Symbol’s value as variable is void: x
> (setq lexical-binding t)
t
> (reazon-run* q (_five q))
*** Eval error ***  Symbol’s value as variable is void: x
> (reazon-defrel _five (x) (reazon-== x 5))
_five
> (reazon-run* q (_five q))
(5)

Is the equality operator (reazon-)== an assertion that two things are the same, or an assignment that makes two things the same?

That is a deep question.

It’s a pain in the ass to use the reazon- namespace prefix all the time, especially for an operator as common as reazon-==.

I know. I’m working on it.

Can Reazon be used to solve dusty old logic puzzles?

Yes. Consider the following dusty old logic puzzle[fn:2]:

Five schoolgirls sat for an examination. Their parents – so they thought – showed an undue degree of interest in the result. They therefore agreed that, in writing home about the examination, each girl should make one true statement and one untrue one. The following are the relevant passages from their letters:

> Betty: “Kitty was second in the examination. I was only third.”

> Ethel: “You’ll be glad to hear that I was on top. Joan was second.”

> Joan: “I was third, and poor old Ethel was bottom.”

> Kitty: “I came out second. Mary was only fourth.”

> Mary: “I was fourth. Top place was taken by Betty.”

What in fact was the order in which the five girls were placed?

Representing the exam results as a five element list ordered from first to last, this puzzle can be transformed into the following query:

(reazon-run* q
  (reazon-fresh (a b c d e)
    ;; Betty: "Kitty was second in the examination. I was only third."
    (reazon-disj
     (reazon-== q `(,a kitty ,c ,d ,e))
     (reazon-== q `(,a ,b betty ,d ,e)))
    ;; Ethel: "You'll be glad to hear that I was on top. Joan was second."
    (reazon-disj
     (reazon-== q `(ethel ,b ,c ,d ,e))
     (reazon-== q `(,a joan ,c ,d ,e)))
    ;; Joan: "I was third, and poor old Ethel was bottom."
    (reazon-disj
     (reazon-== q `(,a ,b joan ,d ,e))
     (reazon-== q `(,a ,b ,c ,d ethel)))
    ;; Kitty: "I came out second. Mary was only fourth."
    (reazon-disj
     (reazon-== q `(,a kitty ,c ,d ,e))
     (reazon-== q `(,a ,b ,c mary ,e)))
    ;; Mary: "I was fourth. Top place was taken by Betty."
    (reazon-disj
     (reazon-== q `(,a ,b ,c mary ,e))
     (reazon-== q `(betty ,b ,c ,d ,e))))
  (reazon-subseto '(betty ethel joan kitty mary) q))

((ethel kitty joan mary betty)
 (ethel kitty joan mary betty)
 (kitty joan betty mary ethel))

That query yielded multiple results (two, in fact, with one duplicate) because Reazon lacks a disequality operator, making it difficult to encode negation. The puzzle says that each girl made one true statement and one false statement. Our use of the disjunction operator requires that at least one of the two statements be true, but doesn’t preclude them from both being true. Thus the query fails to pin down the correct answer.

With a little bit of boring manual labor, it’s possible to get something that works:

(reazon-run* q
  (reazon-fresh (a b c d e)
    ;; Betty: "Kitty was second in the examination. I was only third."
    (reazon-disj
     (reazon-== q `(,a kitty ,c ,d ,e))
     (reazon-== q `(,a ,b betty ,d ,e)))
    ;; Ethel: "You'll be glad to hear that I was on top. Joan was second."
    (reazon-disj
     (reazon-== q `(ethel ,b ,c ,d ,e))
     (reazon-== q `(,a joan ,c ,d ,e)))
    ;; Joan: "I was third, and poor old Ethel was bottom."
    (reazon-disj
     (reazon-== q `(,a ,b joan ,d ,e))
     (reazon-== q `(,a ,b ,c ,d ethel)))
    ;; Kitty: "I came out second. Mary was only fourth."
    (reazon-disj
     ;; Explicity enumerate possibilities to simulate negation.
     (reazon-disj
      (reazon-== q `(mary kitty ,c ,d ,e))
      (reazon-== q `(,a kitty mary ,d ,e))
      (reazon-== q `(,a kitty ,c ,d mary)))
     (reazon-disj
      (reazon-== q `(kitty ,b ,c mary ,e))
      (reazon-== q `(,a ,b kitty mary ,e))
      (reazon-== q `(,a ,b ,c mary kitty))))
    ;; Mary: "I was fourth. Top place was taken by Betty."
    (reazon-disj
     (reazon-== q `(,a ,b ,c mary ,e))
     (reazon-== q `(betty ,b ,c ,d ,e))))
  (reazon-subseto '(betty ethel joan kitty mary) q))

((kitty joan betty mary ethel))

See Solving Logic Puzzles in Emacs with Reazon.

Can Reazon be used as a Sudoku solver?

Yes. See the included file reazon-sudoku.el.

Can Reazon be used as a theorem prover?

Yes. See:

• Generating Sentences of Modal Logic
• Generating Propositional Logic Proofs

Can Reazon be used as part of a static analyzer / linter?

Sure. Suppose you wanted to write a rule that says any expression of the form (if condition (progn body-1 body-2 ...)) should be rewritten as (when condition body-1 body-2 ...) [fn:3]. This could be encoded as something like the following:

(reazon-defrel if-without-else-becomes-when (exp out)
  (reazon-fresh (condition body)
    (reazon-== exp `(if ,condition (progn ,@body)))
    (reazon-== out `(when ,condition ,@body))))

Transforming an expression is merely a matter of running the relation rule against it:

(let ((exp '(if condition (progn body-1 body-2))))
  (reazon-run* q
    (if-without-else-becomes-when exp q)))

((when condition body-1 body-2))

That looks like simple pattern matching. Wouldn’t it be easier just to use pcase?

pcase only goes one way. What if you wanted to go the other direction?

(let ((exp '(when condition body-1 body-2)))
  (reazon-run* q
    (if-without-else-becomes-when q exp)))

((if condition
     (progn body-1 body-2)))

That’s right: with Reazon, you can run your linter backwards to systematically generate worse code! If that isn’t a killer app, I don’t know what is.

Can Reazon be used as part of a scheduler, say, in conjuction with Org Mode?

That sounds like a neat idea!

Does Reazon support Prolog-style database queries?

Not directly, but it’s possible to simulate them. In Prolog, a goal is a predicate applied to some arguments, and a predicate is defined by a set of one or more clauses, where a clause is list of one or more goals. A fact is a clause consisting of a single goal and a rule is a clause consisting of two or more goals. The first goal of a rule is called the head and the rest are collectively called the body. (Actually, we can simply define a fact as a rule with an empty body). The head of a rule holds when each goal in its body does, and a predicate holds when any of its clauses do.

Now, suppose we want to define the predicate likes [fn:4]. There are some primitive facts about who likes whom:

likes(kim, robin)
likes(sandy, lee)
likes(sandy, kim)
likes(robin, cats)
likes(?x, ?x)

And there are some rules extending the likes predicate:

likes(sandy, ?x) :- likes(?x, cats)
likes(kim, ?x) :- likes(?x, lee), likes(?x, kim)

A predicate holds when any of its clauses do, and a clause holds when each goal in its body does. Thus the truth of a predicate is defined by a disjunction of conjunctions. Well, that’s exactly what conde does!

(reazon-defrel likes (a b)
  (reazon-conde
   ((reazon-== a 'kim) (reazon-== b 'robin))
   ((reazon-== a 'sandy) (reazon-== b 'lee))
   ((reazon-== a 'sandy) (reazon-== b 'kim))
   ((reazon-== a 'robin) (reazon-== b 'cats))
   ((reazon-fresh (x)
      (reazon-== a 'sandy)
      (reazon-== b x)
      (likes x 'cats)))
   ((reazon-fresh (x)
      (reazon-== a 'kim)
      (reazon-== b x)
      (likes x 'lee)
      (likes x 'kim)))
   ((reazon-fresh (x)
      (reazon-== a x)
      (reazon-== b x)))))

Defining a predicate in this way makes it inconvenient to update it with new rules and facts, but it is nonetheless logically sufficient.

See the test file test/reazon-test-prolog.el for an extended example involving a personnel records database.

Footnotes

[fn:1] This example is used by every introduction to logic programming I’ve ever seen, including those for Prolog.

[fn:2] This is SICP exercise 4.42.

[fn:3] See the Emacs Lisp Style Guide.

[fn:4] This example comes from the logic programming chapter of PAIP.