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.

`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.

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 `jackal`

s and `leopard`

s,
and we desire to keep gentle `panda`

s 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 `panda`

s 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)))