Core miniKanren extends Scheme with three operations:
There is also
run, which serves as an interface between
Scheme and miniKanren, and whose value is a list.
== unifies two terms.
syntactically looks like
lambda, introduces lexically-scoped
Scheme variables that are bound to new logic variables;
also performs conjunction of the relations within its body. Thus
would introduce logic variables
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
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
rightmost example, the
y introduced by
different from the
y introduced by
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
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
_.0 in the
_.1 in the
second. The argument
run denotes the
maximum length of the resultant list. If
is used instead, then there is no maximum imposed. This can easily lead to
If we replace
* by a natural number
n-element list of alternating
#t's is returned.
The first answer is produced by the first
conde clause, which associates
To produce the second answer, the second
clause is tried. Since
conde clauses are independent, the association between
#f made in the first clause is forgotten---we say that
q has been
refreshed. In the third
anyo, which tries
gan unbounded number of times.
Consider the first example,
which does not terminate because the call to
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.)
Here the values
interleaved; our use of
anyo ensures that this sequence is
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
(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
=/= (previously described in the
context of the cKanren constraint logic programming framework
cKanren); type constraints
numbero, which are the miniKanren equivalent
number? type predicates; and
absento}, which ensures a symbol
tag does not occur
in a term
The single answer
(_.0 (sym _.0))
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
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
unbound, and that
p cannot be associated with
r is associated with
We would get the same answer if we were to replace
(=/= '(1 2) `(,p ,r)) by either
(=/= '((1) (2)) `((,p) (,r)))
(=/= `((1) (,r)) `((,p) (2))).
Now consider the
If we also associate
run expression fails.
Now consider what happens when
(== 2 r) is replaced
(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
Assume we have a term
q containing predators such as
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,
y, cannot be associated with a term that contains the
panda. If we violate this constraint by associating
panda (or with a list containing
no longer returns any answers, keeping the
x is known to be a symbol, the
x can be simplified to a disequality constraint
The answer still contains the full
absento constraint on
y; violating this constraint does indeed cause failure.