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
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.
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
We can get back more interesting values by unifying the query variable with another term.
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.
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.
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.
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.
Consider the first example,
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
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,
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.
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.
Try replacing all occurrences of symbolo by numbero in the
three examples above.
Next we consider the disequality constraint =/=.
The answer states that p remains unbound, but cannot be associated with
1. Of course, violating the constraint leads to failure:
A slightly more complicated example is a disequality constraint between two lists.
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
If we also associate r with 2, the run expression fails.
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.
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.
If x is known to be a symbol, the absento
constraint on x can be simplified to a disequality constraint
between x and panda.
The answer still contains the full absento constraint on
y; violating this constraint does indeed cause failure.