sī-Kanren, a microKanren implementation in Common Lisp, with disequality, numbero, symbolo and absento constraints

sī-Kanren is based on the 2013 Scheme Workshop paper by Jason Hemann and Dan Friedman. Other resources are available on the miniKanren website. It's written in "pure" and simple Common Lisp, without external libraries like pmatch, guard or things like that, nor record types or structs. The constraint store in fact, as a whole, has the form:

cs = '(((s) . c) (d) (t) (a))

where s is the substitution, c the counter, d the disequality store, t the type store and a the absento store.

For more information:

• Excellent survey paper on unification: Kevin Knight.
• Disunification papers: Hubert Comon , Pierre Lescanne.
  • Hubert Comon
• Combining Unification and Disunification Algorithms: Klaus U. Schulz.
• And, above all, the miniKanren uncourse series, by William Byrd!

Features

sī-Kanren includes:

1. core miniKanren (fresh, conde, ==).
2. =/= constraint, and thus it's the first microKanren written in Common Lisp with this feature (at least, as far as I know).
3. Symbolo, numbero and absento constraints, the latter in the restricted version, as per the paper A tutorial reconstruction of miniKanren with constraints Bharathi Ramana Joshi, William E. Byrd, where the first argument is required to be a symbol only.
4. Reification of all the logic queries variables x x0... in (run _ (x x0...)...). It looks like a trick of magic too beautiful to not include it. 🪄
5. Interactive request of a solution/s, with runi.
6. Pretty formatting of the answer/s.

Installation

sī-Kanren is a library in Quicklisp. To load it, use:

(ql:quickload "si-kanren")

Usage¹

Many examples can be found in the playground file.

Credits

• Inspiration for a simple implementation in Common Lisp, from cl-microkanren.

• Inspiration for the implementation of the disequality store, from microKanren-sagittarius.

• I took the Zebra Puzzle example here².

• The version of the nlet-tail macro (among others things), from Let Over Lambda, by Doug Hoyte (@hoytech).

• And, of course, last but not least, many thank's to @webyrd for his sensational work!

As for the name, sī is the Chinese unit of measurement for 10 micrometers: since compared to microKanren sī-Kanren also contains the disequality store, plus the types and absento constraints, it seemed to me a fair way to give credit to this system. 😁 And since I think it can be pronounced like a c (more or less...), as in Common Lisp, the circle closes³.

Footnotes

1. Tested on SBCL v. 2.3.0 ↩

2. @alex-hhh Hope it's ok for you! Here's the CC BY-NC-SA 4.0 license link. ↩

3. Cit.: The Stand, Stephen King ↩