miniKanren: an interactive Tutorial

Fork me on GitHub

Core miniKanren

Core miniKanren extends Scheme with three operations: ==, fresh, and conde. There is also run, which serves as an interface between Scheme and miniKanren, and whose value is a list.

== unifies two terms. fresh, which syntactically looks like lambda, introduces lexically-scoped Scheme variables that are bound to new logic variables; fresh also performs conjunction of the relations within its body. Thus

(fresh (x y z) (== x z) (== 3 y))

would introduce logic variables x, y, and z, then associate x with z and y with 3. This, however, is not a legal miniKanren program---we must wrap a run around the entire expression.

(run 1 (q) (fresh (x y z) (== x z) (== 3 y)))

The value returned is a list containing the single value (_.0); we say that _.0 is the reified value of the unbound query variable q and thus represents any value. q also remains unbound in

(run 1 (q) (fresh (x y) (== x q) (== 3 y)))

We can get back more interesting values by unifying the query variable with another term.

(run 1 (y) (fresh (x z) (== x z) (== 3 y)))
(run 1 (q) (fresh (x z) (== x z) (== 3 z) (== q x)))
(run 1 (y) (fresh (x y) (== 4 x) (== x y)) (== 3 y))

Each of these examples returns (3); in the last example, the y introduced by fresh is different from the y introduced by run.

A run expression can return the empty list, indicating that the body of the expression is logically inconsistent.

(run 1 (x) (== 4 3))
(run 1 (x) (== 5 x) (== 6 x))

We say that a logically inconsistent relation fails, while a logically consistent relation, such as (== 3 3), succeeds.

conde, which resembles cond syntactically, is used to produce multiple answers. Logically, conde can be thought of as disjunctive normal form: each clause represents a disjunct, and is independent of the other clauses, with the relations within a clause acting as the conjuncts. For example, this expression produces two answers.

(run 2 (q) (fresh (w x y) (conde ((== `(,x ,w ,x) q) (== y w)) ((== `(,w ,x ,w) q) (== y w)))))

Although the two conde lines are different, the values returned are identical. This is because distinct reified unbound variables are assigned distinct subscripts, increasing from left to right—the numbering starts over again from zero within each answer, which is why the reified value of x is _.0 in the first answer but _.1 in the second. The argument 2 in run denotes the maximum length of the resultant list. If run* is used instead, then there is no maximum imposed. This can easily lead to infinite loops.

(run* (q) (let loop () (conde ((== #f q)) ((== #t q)) ((loop)))))

If we replace * by a natural number n, then an n-element list of alternating #f's and #t's is returned. The first answer is produced by the first conde clause, which associates q with #f. To produce the second answer, the second conde clause is tried. Since conde clauses are independent, the association between q and #f made in the first clause is forgotten---we say that q has been refreshed. In the third conde clause, q is refreshed again.

We now look at several interesting examples that rely on anyo, which tries g an unbounded number of times.
(define anyo (lambda (g) (conde (g) ((anyo g)))))

Consider the first example,

(run* (q) (conde ((anyo (== #f q))) ((== #t q))))

which does not terminate because the call to anyo succeeds an unbounded number of times. If * were replaced by 5, then we would get (#t #f #f #f #f). (The user should not be concerned with the order of the answers produced.)

Now consider

(run 10 (q) (anyo (conde ((== 1 q)) ((== 2 q)) ((== 3 q)))))

Here the values 1, 2, and 3 are interleaved; our use of anyo ensures that this sequence is repeated indefinitely.

Even if a relation within a conde clause loops indefinitely (or diverges), other conde clauses can contribute to the answers returned by a run expression. For example,

(run 3 (q) (let ((nevero (anyo (== #f #t)))) (conde ((== 1 q)) (nevero) ((conde ((== 2 q)) (nevero) ((== 3 q)))))))

returns (1 2 3). Replacing run 3 with run 4 would cause divergence, since nevero would loop indefinitely looking for the non-existent fourth answer.

Additional Constraint Operators

We extend core miniKanren with four constraint operators: the disequality constraint =/= (previously described in the context of the cKanren constraint logic programming framework); type constraints symbolo and numbero, which are the miniKanren equivalent of Scheme's symbol? and number? type predicates; and absento, which ensures a symbol tag does not occur in a term t.

(run* (q) (symbolo q))

The single answer (_.0 (sym _.0)) indicates that q remains unbound, and also that q represents a symbol. Any attempt to associate q with a non-symbol value should therefore lead to failure.

(run* (q) (symbolo q) (== 4 q))
(run* (q) (symbolo q) (numbero q))

Try replacing all occurrences of symbolo by numbero in the three examples above.

Next we consider the disequality constraint =/=.

(run* (p) (=/= p 1))

The answer states that p remains unbound, but cannot be associated with 1. Of course, violating the constraint leads to failure:

(run* (p) (=/= 1 p) (== 1 p))

A slightly more complicated example is a disequality constraint between two lists.

(run* (q) (fresh (p r) (=/= '(1 2) `(,p ,r)) (== `(,p ,r) q)))

The answer states that p and r are unbound, and that p cannot be associated with 1 while r is associated with 2.

We would get the same answer if we were to replace (=/= '(1 2) `(,p ,r)) by either (=/= '((1) (2)) `((,p) (,r))) or (=/= `((1) (,r)) `((,p) (2))).

Now consider the run expression

(run* (q) (fresh (p r) (=/= '(1 2) `(,p ,r)) (== 1 p) (== `(,p ,r) q)))

If we also associate r with 2, the run expression fails.

(run* (q) (fresh (p r) (=/= '(1 2) `(,p ,r)) (== 1 p) (== 2 r) (== `(,p ,r) q)))

Now consider what happens when (== 2 r) is replaced by (symbolo r) in the previous example. Then the run expression succeeds with an answer which states that r can only be associated with a symbol. The reified constraint (=/= ((_.0 2))) (stating that r cannot be associated with 2) is not included in the answer, since it is subsumed by the constraint that r must be a symbol.

Finally we consider absento, which ensures a symbol tag does not appear in a term t. Assume we have a term q containing predators such as jackals and leopards, and we desire to keep gentle pandas out of this dangerous term. We can use absento to ensure that this will occur.

(run* (q) (fresh (x y) (== `(jackal (,y leopard ,x)) q) (absento 'panda q)))

The answer states that the two unbound variables, x and y, cannot be associated with a term that contains the term panda. If we violate this constraint by associating x with panda (or with a list containing panda), the run expression no longer returns any answers, keeping the pandas safe.

(run* (q) (fresh (x y) (== `(jackal (,y leopard ,x)) q) (absento 'panda q) (== 'panda x)))

If x is known to be a symbol, the absento constraint on x can be simplified to a disequality constraint between x and panda.

(run* (q) (fresh (x y) (== `(jackal (,y leopard ,x)) q) (absento 'panda q) (symbolo x)))

The answer still contains the full absento constraint on y; violating this constraint does indeed cause failure.

(run* (q) (fresh (x y z) (== `(jackal (,y leopard ,x)) q) (absento 'panda q) (symbolo x) (== `(c ,z d) y) (== 'panda z)))