miniKanren, Live and Untagged

Quine Generation via Relational Interpreters

(Programming Pearl)

William E. Byrd Eric Holk Daniel P. Friedman

School of Informatics and Computing, Indiana University, Bloomington, IN 47405
{webyrd,eholk,dfried}@cs.indiana.edu

Abstract evaluating literals, such as numbers and booleans. A classic

We present relational interpreters for several subsets of non-trivial quine (Thompson II) is:
Scheme, written in the pure logic programming language (define quinec
miniKanren. We demonstrate these interpreters running ’((lambda (x)
“backwards”—that is, generating programs that evaluate (list x (list (quote quote) x)))
to a specified value—and show how the interpreters can (quote
trivially generate quines (programs that evaluate to them- (lambda (x)
selves). We demonstrate how to transform environment- (list x (list (quote quote) x))))))
passing interpreters written in Scheme into relational inter- We can easily verify that quinec evaluates to itself:
preters written in miniKanren. We show how constraint ex-
tensions to core miniKanren can be used to allow shadowing (equal? (eval quinec ) quinec ) ⇒ #t
of the interpreter’s primitive forms (using the absent o tree
For decades programmers have amused themselves by
constraint), and to avoid having to tag expressions in the
writing quines in countless programming languages. Some
languages being interpreted (using disequality constraints
quines, such as those featured in the International Obfus-
and symbol/number type-constraints), simplifying the in-
cated C Code Contest (Broukhis et al.), are intentionally
terpreters and eliminating the need for parsers/unparsers.
baroque. Here we demonstrate a disciplined approach to the
We provide four appendices to make the code in the paper
problem: we show how to translate a standard environment-
completely self-contained. Three of these appendices contain
passing interpreter written as a Scheme function into a re-
new code: the complete implementation of core miniKanren
lation in the pure logic programming language miniKanren
extended with the new constraints; an extended relational
(Byrd 2009; Friedman et al. 2005), then show how this re-
interpreter capable of running factorial and doing list pro-
lational interpreter can be used, without modification, to
cessing; and a simple pattern matcher that uses Dijkstra
trivially generate quines.1
guards. The other appendix presents our preferred version of
We also show how to generate twines (twin quines), which
code that has been presented elsewhere: the miniKanren re-
are distinct programs p and q that evaluate to each other,
lational arithmetic system used in the extended interpreter.
and thrines, which are distinct programs p, q, and r such
Categories and Subject Descriptors D.1.6 [Program- that p evaluates to q, q evaluates to r , and r evaluates to p.
ming Techniques]: Logic Programming; D.1.1 [Program- While generating quines is fun and interesting, our ap-
ming Techniques]: Applicative (Functional) Programming proach also illustrates advanced techniques of relational pro-
gramming, such as translating functional programs into re-
General Terms Languages lational programs, and using constraints to avoid having to
Keywords quines, Scheme, miniKanren, relational pro- tag the expressions being interpreted. This last point is espe-
gramming, logic programming, interpreters, tagging cially important, as tagging implies the need to write parsers
and unparsers, and because tagging the application line of
the interpreter greatly complicates the handling of quote
1. Introduction and list. Our use of constraints also has the important ben-
A quine is a program that evaluates to itself (Hofstadter efit of properly handling shadowing of the interpreter’s built-
1979; Thompson II); the simplest Scheme quines are self- in primitives, such as list, quote, and lambda.
Our approach requires adding several constraint oper-
ators to core miniKanren. We have previously presented
disequality constraints in cKanren (Alvis et al. 2011), a
general constraint logic programming (Apt 2003) frame-
work inspired by miniKanren; the symbol o , number o , and

1 Forreaders already familiar with miniKanren, the punchline of

the paper can be summarized by the one-liner:
(equal? (caar (run1 (q) (eval-exp o q ’() q))) quinec ) ⇒ #t
(More accurately, the generated quine is α-equivalent to quinec .)

1
absent o constraints we introduce are also straightforward to while those wishing to learn more about miniKanren should
implement in cKanren. However, we have found that core see Byrd (2009), Byrd and Friedman (2006) (from which this
miniKanren augmented with these four constraints is suf- subsection has been adapted), and Friedman et al. (2005).
ficient for implementing a wide variety of interesting pro-
grams, including interpreters and inferencers. This extended 2.1 miniKanren Refresher
miniKanren is conceptually simpler than cKanren, and its Our code uses the following typographic conventions. Lexi-
implementation is easier to understand and modify. Pro- cal variables are in italic, forms are in boldface, and quoted
grammers needing to use domain-specific constraints, such symbols are in sans serif. By our convention, names of rela-
as arithmetic over finite domains (CLP(FD)), will find that tions end with a superscript o—for example any o , which is
the techniques described here, up to and including quine entered as anyo. Some relational operators do not follow this
generation, work equally well in cKanren. convention: ≡ (entered as ==), conde (entered as conde),
Our paper makes the following contributions: and fresh. Similarly, (run5 (q) body) and (run∗ (q) body)
• We extend the miniKanren core language with four con- are entered as (run 5 (q) body) and (run* (q) body).2
straint operators (section 2.2): the disequality constraint Core miniKanren extends Scheme with three operators:
6≡; type constraints symbol o and number o , which are sim- ≡, fresh, and conde . (Four additional constraint operators
ilar in spirit to Scheme’s symbol? and number? pred- are introduced in section 2.2.) There is also run, which
icates; and the tree constraint absent o , which ensures serves as an interface between Scheme and miniKanren, and
a symbol tag does not occur inside a term t. These whose value is a list.
constraints are extremely useful when writing logic pro- ≡ unifies two terms. fresh, which syntactically looks
grams, especially interpreters and type inferencers. like lambda, introduces lexically-scoped Scheme variables
• We describe and demonstrate our methodology for trans- that are bound to new logic variables; fresh also performs
lating interpreters from Scheme to miniKanren (sec- conjunction of the relations within its body. Thus
tion 3). Our methodology is equally useful for translating (fresh (x y z ) (≡ x z ) (≡ 3 y))
type inferencers.
• We show how 6≡, symbol o , and number o can be used when would introduce logic variables x , y, and z , then associate x
writing an interpreter (or type inferencer) to avoid having with z and y with 3. This, however, is not a legal miniKanren
to tag expressions in the language being interpreted, and program—we must wrap a run around the entire expression.
how absent o can be used to allow shadowing of primitive (run1 (q) (fresh (x y z ) (≡ x z ) (≡ 3 y))) ⇒ ( 0 )
forms (section 3).
• The value returned is a list containing the single value 0 ; we
We present relational interpreters for three subsets
say that 0 is the reified value of the unbound query variable
of Scheme: the call-by-value λ-calculus (section 3);
q and thus represents any value. q also remains unbound in
λ-calculus extended with list and quote (section 4);
and an extended language supporting pairs, condition- (run1 (q) (fresh (x y) (≡ x q) (≡ 3 y))) ⇒ ( 0 )
als, and arithmetic operators, and capable of running
factorial (appendix A). The relational arithmetic sys- We can get back more interesting values by unifying the
tem (appendix B) used in the third interpreter was first query variable with another term.
presented in Friedman et al. (2005); we include it for (run1 (y) (run1 (q) (run1 (y)
completeness. (fresh (x z ) (fresh (x z ) (fresh (x y)
• We demonstrate these interpreters running “backwards” (≡ x z ) (≡ x z ) (≡ 4 x )
(generating input expressions from the expected output), (≡ 3 y))) (≡ 3 z ) (≡ x y))
and show how the interpreters supporting list and quote (≡ q x ))) (≡ 3 y))
can be used to trivially generate quines (section 5 and
appendix A). Each of these examples returns (3); in the rightmost ex-
ample, the y introduced by fresh is different from the y
• We provide a complete, concise, and easily modifi- introduced by run.
able implementation of core miniKanren extended with A run expression can return the empty list, indicating
6≡, symbol o , number o , and absent o constraints (ap- that the body of the expression is logically inconsistent.
pendix D).
• We provide a generalized version of the pmatch pattern (run1 (x ) (≡ 4 3)) ⇒ ()
matcher first presented in Byrd and Friedman (2007); the (run1 (x ) (≡ 5 x ) (≡ 6 x )) ⇒ ()
updated pmatch, now called dmatch (appendix C), is
based on Dijkstra guards (Dijkstra 1975). This gener- We say that a logically inconsistent relation fails, while a
alized pattern matcher properly handles quote expres- logically consistent relation, such as (≡ 3 3), succeeds.
sions, which is important when writing evaluators, infer- conde , which resembles cond syntactically, is used to
encers, and reducers. produce multiple answers. Logically, conde can be thought
of as disjunctive normal form: each clause represents a dis-
We begin by introducing the extended miniKanren lan-
junct, and is independent of the other clauses, with the rela-
guage we will use to write the relational interpreters.
tions within a clause acting as the conjuncts. For example,
this expression produces two answers.
2. The Extended miniKanren Language
In this section we briefly review the core miniKanren lan- 2 It is conventional in Scheme for the names of predicates to
guage (section 2.1), then introduce the 6≡, symbol o , number o , end with the ‘?’ character. We have therefore chosen to end the
and absent o constraints used in the relational interpreters names of miniKanren goals with a superscript o, which is meant
(section 2.2). Readers already familiar with miniKanren can to resemble the top of a ‘?’. The superscript e in conde stands
safely skip to section 2.2 to learn about the new constraints, for ‘every,’ since every conde clause may contribute answers.

2
(run2 (q) (run3 (q)
(fresh (w x y) (let ((never o (any o (≡ #f #t))))
(conde (conde
((≡ ‘(,x ,w ,x ) q) ((≡ 1 q))
(≡ y w )) (never o )
((≡ ‘(,w ,x ,w ) q) ((conde
(≡ y w ))))) ⇒ (( 0 1 0 )( 0 1 0 )) ((≡ 2 q))
(never o )
Although the two conde lines are different, the values re- ((≡ 3 q)))))))
turned are identical. This is because distinct reified unbound
variables are assigned distinct subscripts, increasing from returns (1 2 3). Replacing run3 with run4 would cause
left to right—the numbering starts over again from zero divergence, since never o would loop indefinitely looking for
within each answer, which is why the reified value of x is the non-existent fourth answer.
0 in the first answer but 1 in the second. The superscript
2 in run denotes the maximum length of the resultant list. 2.2 Additional Constraint Operators
If the superscript ∗ is used, then there is no maximum im- We extend core miniKanren with four constraint opera-
posed. This can easily lead to infinite loops. tors: the disequality constraint 6≡ (previously described in
the context of the cKanren constraint logic programming
(run∗ (q) framework (Alvis et al. 2011)); type constraints symbol o and
(let loop () number o , which are the miniKanren equivalent of Scheme’s
(conde symbol? and number? type predicates; and absent o , which
((≡ #f q)) ensures a symbol tag does not occur in a term t.
((≡ #t q)) We begin with the symbol o type constraint.
((loop))))) ⇒ ⊥
(run∗ (q) (symbol o q)) ⇒ (( 0 (sym 0 )))
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 The single answer ( 0 (sym 0 )) indicates that q remains
produced by the first conde clause, which associates q with unbound, and also that q represents a symbol. Any attempt
#f. To produce the second answer, the second conde clause is to associate q with a non-symbol value should therefore lead
tried. Since conde clauses are independent, the association to failure.
between q and #f made in the first clause is forgotten—we (run∗ (q) (run∗ (q)
say that q has been refreshed. In the third conde clause, q (symbol o q) (symbol o q)
is refreshed again. (≡ 4 q)) ⇒ () (number o q)) ⇒ ()
We now look at several interesting examples that rely on
If we were to replace all occurrences of symbol o by
any o , which tries g an unbounded number of times.
number o in the three examples above, the new answers pro-
(define any o duced would be (( 0 (num 0 ))), (4), and (( 0 (num 0 ))),
(lambda (g) respectively.
(conde Next we consider the disequality constraint 6≡.
(g) (run∗ (p) (6≡ p 1)) ⇒ (( 0 (6≡ (( 0 1)))))
((any o g)))))
The answer states that p remains unbound, but cannot be
Consider the first example, associated with 1. Of course, violating the constraint leads
to failure:
(run∗ (q)
(conde (run∗ (p) (6≡ 1 p) (≡ 1 p)) ⇒ ()
((any o (≡ #f q)))
((≡ #t q)))) A slightly more complicated example is a disequality
constraint between two lists.
which does not terminate because the call to any o succeeds
an unbounded number of times. If ∗ were replaced by 5, (run∗ (q)
then we would get (#t #f #f #f #f). (The user should not be (fresh (p r )
concerned with the order of the answers produced.) (6≡ ’(1 2) ‘(,p ,r ))
Now consider (≡ ‘(,p ,r ) q))) ⇒ ((( 0 1 ) (6≡ (( 0 1) ( 1 2)))))

(run10 (q) The answer states that p and r are unbound, and that
(any o p cannot be associated with 1 while r is associated with
(conde 2 (and the other way around). We would get the same
((≡ 1 q)) answer if we were to replace (6≡ ’(1 2) ‘(,p ,r )) by either
((≡ 2 q)) (6≡ ’((1) (2)) ‘((,p) (,r ))) or (6≡ ‘((1) (,r )) ‘((,p) (2))).
((≡ 3 q))))) ⇒ (1 2 3 1 2 3 1 2 3 1) Now consider the run expression

Here the values 1, 2, and 3 are interleaved; our use of any o (run∗ (q)
ensures that this sequence is repeated indefinitely. (fresh (p r )
Even if a relation within a conde clause loops indefinitely (6≡ ’(1 2) ‘(,p ,r ))
(or diverges), other conde clauses can contribute to the (≡ 1 p)
answers returned by a run expression. For example, (≡ ‘(,p ,r ) q))) ⇒ (((1 0 ) (6≡ (( 0 2)))))

3
If we also associate r with 2, the run expression fails. 3. Translating an Interpreter from
(run∗ (q)
Scheme to miniKanren
(fresh (p r ) In this section we start with a standard environment-passing
(6≡ ’(1 2) ‘(,p ,r )) interpreter for the call-by-value λ-calculus, then show how
(≡ 1 p) the interpreter can be translated into miniKanren in order
(≡ 2 r ) to run “backwards.”
(≡ ‘(,p ,r ) q))) ⇒ () We begin by defining variable lookup in an environment
represented as an association list.
Now consider what happens when (≡ 2 r ) is replaced
by (symbol o r ) in the previous example. Then the run ex- (define lookup
pression succeeds with the answer (((1 0 ) (sym 0 ))) which (lambda (x env )
states that r can only be associated with a symbol. The (dmatch env
reified constraint (6≡ (( 0 2))) (stating that r cannot be as- (() (error ’lookup "unbound variable"))
sociated with 2) is not included in the answer, since it is (((,y . ,v ) . ,rest) (guard (eq? y x ))
subsumed by the constraint that r must be a symbol. v)
Finally we consider absent o , which ensures a symbol tag (((,y . ,v ) . ,rest) (guard (not (eq? y x )))
does not appear in a term t. Assume we have a term q (lookup x rest)))))
containing predators such as jackals and leopards, and we
desire to keep gentle pandas out of this dangerous term. We lookup uses dmatch (appendix C), a simple pattern matcher
can use absent o to ensure that this will occur. with guards in the style of Dijkstra’s Guarded Commands
(Dijkstra 1975). dmatch ensures that the patterns and op-
(run∗ (q) tional guards of different clauses do not overlap.3 This non-
(fresh (x y) overlapping property ensures that the ordering of the clauses
(≡ ‘(jackal (,y leopard ,x )) q) does not matter, and is required for writing correct relational
(absent o ’panda q))) programs (Byrd 2009). By ensuring the non-overlapping
⇒ property holds in the Scheme version of the interpreter, we
(((jackal ( 0 leopard 1 )) simplify the translation to miniKanren.
(absent panda 0 ) Now that we have defined lookup, we can write our simple
(absent panda 1 ))) interpreter using dmatch.
The answer states that the two unbound variables, x and
(define eval-exp
y, cannot be associated with a term that contains the term
(lambda (exp env )
panda. If we violate this constraint by associating x with
(dmatch exp
panda (or with a list containing panda), the run expression
((,rator ,rand )
no longer returns any answers, keeping the pandas safe.
(let ((proc (eval-exp rator env ))
(run∗ (q) (arg (eval-exp rand env )))
(fresh (x y) (dmatch proc
(≡ ‘(jackal (,y leopard ,x )) q) ((closure ,x ,body ,env2 )
(absent o ’panda q) (eval-exp body ‘((,x . ,arg) . ,env2 ))))))
(≡ ’panda x ))) ⇒ () ((lambda (,x ) ,body)
(guard (symbol? x ) (not-in-env? ’lambda env ))
If x is known to be a symbol, the absent o constraint on x ‘(closure ,x ,body ,env ))
can be simplified to a disequality constraint between x and (,x (guard (symbol? x )) (lookup x env )))))
panda.
(define not-in-env?
(run∗ (q) (lambda (x env )
(fresh (x y) (dmatch env
(≡ ‘(jackal (,y leopard ,x )) q) (() #t)
(absent o ’panda q) (((,y . ,v ) . ,rest) (guard (eq? y x )) #f)
(symbol o x ))) (((,y . ,v ) . ,rest) (guard (not (eq? y x )))
⇒ (not-in-env? x rest)))))
(((jackal ( 0 leopard 1 ))
(6≡ (( 1 panda))) The guard in eval-exp’s lambda clause includes the test
(absent panda 0 ) (not-in-env? ’lambda env )
(sym 1 )))
When we extend the interpreter in section 4, and again in
The answer still contains the full absent o constraint on y; appendix A, we will use a similar not-in-env? test in the
violating this constraint does indeed cause failure. guard of every new language form and primitive operator.
This use of not-in-env? serves two critical and related pur-
(run∗ (q)
poses. First, the test ensures that procedure application does
(fresh (x y z )
not overlap with any other clause in the interpreter, such
(≡ ‘(jackal (,y leopard ,x )) q)
as the (quote ,v ) and (list . ,a∗ ) clauses we add in section 4.
(absent o ’panda q)
(symbol o x ) 3 For this reason dmatch does not support else, since the always-
(≡ ‘(c ,z d) y) true implicit test of the else clause overlaps with the patterns and
(≡ ’panda z ))) ⇒ () guards of all other clauses.

4
Second, the test ensures that eval-exp will correctly evaluate clause is unimportant—there are no patterns or guards
expressions in which lambda (or quote or list) is shadowed. within a conde clause, only goals that succeed or fail.5
For example, the interpreter correctly handles shadowing of We can simplify lookup o by removing the first conde
lambda in this definition of Ω. clause (which always fails), and by moving the unification
of env above the conde .
(define Ω
’((lambda (lambda) (lambda lambda)) (define lookup o
(lambda (lambda) (lambda lambda)))) (lambda (x env t)
(fresh (y v rest)
As expected, Ω diverges. (≡ ‘((,y . ,v ) . ,rest) env )
(conde
(eval-exp Ω ’()) ⇒ ⊥ ((≡ y x ) (≡ v t))
((6≡ y x ) (lookup o x rest t))))))
The empty list passed as the second argument to eval-exp
represents the empty environment. With lookup o defined, we can write eval-exp o , which
Here are two more examples showing eval-exp in action: in turn relies on not-in-env o . Since there is no notion of a
guard in miniKanren, we must translate each dmatch guard
(eval-exp (eval-exp into one or more goal expressions; the Scheme predicate
’(((lambda (x) ’((lambda (x) (symbol? x ) becomes the type constraint (symbol o x ), while
(lambda (y) x)) (lambda (y) x)) (not-in-env? ’lambda env ) becomes (not-in-env o ’lambda env ).
(lambda (z) z)) (lambda (z) z))
(lambda (a) a)) ’())
(define eval-exp o
’()) ⇒
(lambda (exp env val )
⇒ (closure y x
(conde
(closure z z ()) ((x . (closure z z ()))))
((fresh (rator rand x body env2 a)
We now have a working λ-calculus interpreter in Scheme (≡ ‘(,rator ,rand ) exp)
that properly handles shadowing, and in which the dmatch (eval-exp o rator env ‘(closure ,x ,body ,env2 ))
clauses can be reordered arbitrarily. Our next task is to (eval-exp o rand env a)
translate the interpreter directly into miniKanren. We start (eval-exp o body ‘((,x . ,a) . ,env2 ) val )))
again with environment lookup; a faithful translation of ((fresh (x body)
lookup into lookup o might be: (≡ ‘(lambda (,x ) ,body) exp)
(symbol o x )
(define lookup o (≡ ‘(closure ,x ,body ,env ) val )
(lambda (x env t) (not-in-env o ’lambda env )))
(conde ((symbol o exp) (lookup o exp env val )))))
((≡ ’() env ) fail )
((fresh (y v rest) not-in-env o differs from lookup o and eval-exp o in that
(≡ ‘((,y . ,v ) . ,rest) env ) (≡ y x ) it does not take an additional argument with respect to
(≡ v t))) the Scheme function from which it was translated. This is
((fresh (y v rest) because not-in-env? is a predicate—the success or failure of
(≡ ‘((,y . ,v ) . ,rest) env ) (6≡ y x ) not-in-env o is equivalent to not-in-env? returning #t or #f,
(lookup o x rest t)))))) respectively, so no “output” argument is needed.

lookup o takes a third argument, t, which corresponds to (define not-in-env o

the value returned by the Scheme function lookup. That is, (lambda (x env )
t represents the term associated with variable x in environ- (conde
ment env . ((≡ ’() env ))
((fresh (y v rest)
(run∗ (q) (lookup o ’y ’((x . foo) (y . bar)) q)) ⇒ (bar) (≡ ‘((,y . ,v ) . ,rest) env )
(6≡ y x )
If x is not bound in env , a call to lookup o will reach the base (not-in-env o x rest))))))
case and fail4 , rather than signaling an error as in lookup.
We can use eval-exp o to generate expression/value pairs.
∗ o
(run (q) (lookup ’w ’((x . foo) (y . bar)) q)) ⇒ ()
(run5 (q)
e o (fresh (e v )
Each cond clause in lookup corresponds to a dmatch
clause in lookup. Instead of pattern matching against env , (eval-exp o e ’() v )
lookup o uses ≡ to unify terms with env . The goal (6≡ y x ) is (≡ ‘(,e → ,v ) q)))
equivalent to the guard (not (eq? y x )) in lookup. As with
dmatch, the order of clauses does not affect the meaning of This run5 expression generates five λ-expressions, and the
a conde expression (but may affect its performance). Unlike closures to which they evaluate.
with dmatch, the order of expressions within a conde
5 Recallfrom section 2.1 that all goals within a conde clause must
4 fail can be defined as (define fail (≡ #f #t)). succeed for the entire clause to succeed.

5
((((lambda ( 0 ) 1 ) ((lambda (x) x) (lambda (y) y)))
→ (closure 0 1 ()))
(sym 0 )) and
((((lambda ( 0 ) 0 ) (lambda ( 1 ) 2 )) ((quote (closure x x ())) (lambda (y) y))
→ (closure 1 2 ()))
(sym 0 1 )) This is because (lambda (x) x) and (quote (closure x x ()))
((((lambda ( 0 ) (lambda ( 1 ) 2 )) (lambda ( 3 ) 4 )) both evaluate to (closure x x ()). We circumvent this issue by
→ (closure 1 2 (( 0 . (closure 3 4 ()))))) declaring that the closure tag is a unique symbol that is not
(6≡ (( 0 lambda))) part of the expression language (a gensym by convention).
(sym 0 1 3 )) We can now translate the quote clause to miniKanren. In
((((lambda ( 0 ) ( 0 0 )) (lambda ( 1 ) 1 )) the Scheme version, we can assume that the user will not
→ (closure 1 1 ())) write expressions containing the closure tag; alternatively,
(sym 0 1 )) we could use an actual gensym for the tag. However, we are
((((lambda ( 0 ) ( 0 0 )) interested in running our relational interpreter backwards,
(lambda ( 1 ) (lambda ( 2 ) 3 ))) and miniKanren has no compunction against generating
→ (closure 2 3 (( 1 . (closure 1 (lambda ( 2 ) 3 ) ()))))) expressions that include a symbol the user cannot or should
(6≡ (( 1 lambda))) not type. We can solve this problem by adding an absent o
(sym 0 1 2 ))) constraint with the symbol closure as the first argument,
ensuring the closure tag does not appear within v .
The 6≡ tags in the answers indicate disequality constraints
between variables and the values they cannot assume. The ((fresh (v )
constraints in the last answer state that 1 cannot be the (≡ ‘(quote ,v ) exp)
symbol lambda and that 0 , 1 , and 2 are symbols. (not-in-env o ’quote env )
To demonstrate eval-exp o running backwards, here are (absent o ’closure v )))
five Scheme expressions that evaluate to the closure from
the last eval-exp example: Like the lambda clause presented in section 3, the quote
clause uses not-in-env o to handle shadowing.
(run5 (q) We now turn our attention to list. For the Scheme inter-
(eval-exp o q ’() ’(closure y x ((x . (closure z z ())))))) preter, list is simply a matter of mapping recursive calls to
⇒ eval-exp over the arguments:
(((lambda (x) (lambda (y) x)) (lambda (z) z))
((lambda (x) (x (lambda (y) x))) (lambda (z) z)) ((list . ,a∗ ) (guard (not-in-env? ’list env ))
(((lambda (x) (lambda (y) x)) (map (lambda (e) (eval-exp e env )) a∗ ))
((lambda ( 0 ) 0 ) (lambda (z) z)))
(sym 0 )) Similarly, we can add list to the miniKanren interpreter:
((((lambda ( 0 ) 0 ) (lambda (x) (lambda (y) x)))
((fresh (a∗ )
(lambda (z) z))
(≡ ‘(list . ,a∗ ) exp)
(sym 0 ))
(not-in-env o ’list env )
(((lambda ( 0 ) 0 )
(absent o ’closure a∗ )
((lambda (x) (lambda (y) x)) (lambda (z) z)))
(proper-list o a∗ env val )))
(sym 0 )))
The constraint (sym 0 ) states that the fresh variable reified Once again, we use the absent o constraint to prevent
as 0 can only be associated with a symbol. miniKanren from generating list expressions that contain
closures. (Of course, a list expression containing λ expres-
4. Extending the Interpreter sions will evaluate to a list containing closures, but the
expression being evaluated must not contain closures.)
We have a relational interpreter, but we cannot yet generate As with the other tagged clauses, proper handling of
quines, or even evaluate quinec from section 1 when running shadowing is ensured through use of not-in-env o . These
forward. We must add quote and list to the interpreter, uses of not-in-env o also serve another purpose: without this
first to the Scheme version, then to miniKanren translation. constraint, the expression (list x ) would be recognized both
Adding quote to the Scheme interpreter is relatively as a procedure application (of whatever procedure might
simple. Since quote means “do not evaluate the argument,” be bound to the variable list), and as a use of the built-in
we simply have to return the argument unmodified. Thus, we primitive list.
can support quote by adding this clause to our interpreter: The list clause relies on proper-list o to ensure a∗ is a
proper list:
((quote ,v ) v )
(define proper-list o
In order to handle shadowing correctly, we must allow the (lambda (exp env val )
user to override the quote form. As with the lambda clause, (conde
we do so by calling not-in-env? within a guard: ((≡ ’() exp)
((quote ,v ) (guard (not-in-env? ’quote env )) v ) (≡ ’() val ))
((fresh (a d v-a v-d )
Unfortunately, quote introduces a new problem: it is (≡ ‘(,a . ,d ) exp)
possible for quoted data to conflict with our representation (≡ ‘(,v-a . ,v-d ) val )
of closures. For example, in the context of our interpreter, (eval-exp o a env v-a)
these two expressions are equivalent: (proper-list o d env v-d ))))))

6
 Our final definition of eval-exp is It is not necessary to test if a rator is valid, since the
application clause will fail if rator is a symbol not bound
(define eval-exp in the environment. If exp is (quote (lambda (x) x)), for
(lambda (exp env ) example, and env contains a binding between quote and
(dmatch exp a closure, then eval-exp o will treat the expression as a
((quote ,v ) (guard (not-in-env? ’quote env )) v ) procedure application, rather than a use of the quote form;
((list . ,a∗ ) (guard (not-in-env? ’list env )) otherwise, if quote is not bound to a closure in env , the
(map (lambda (e) (eval-exp e env )) a∗ )) application clause will fail.
(,x (guard (symbol? x )) (lookup x env ))
((,rator ,rand ) 5. Generating Quines
(guard (rator? rator env ))
(let ((proc (eval-exp rator env )) After much work, we are finally ready to put eval-exp o
(arg (eval-exp rand env ))) through its paces, and generate a quine. The call to eval-
(dmatch proc exp o is trivial—we want to find a Scheme expression q that,
((closure ,x ,body ,env ) when evaluated in the empty environment, returns itself.
(eval-exp body ‘((,x . ,arg) . ,env ))))))
((lambda (,x ) ,body) (run1 (q) (eval-exp o q ’() q)) ⇒
(guard (symbol? x ) (not-in-env? ’lambda env )) ((((lambda ( 0 ) (list 0 (list ’quote 0 )))
‘(closure ,x ,body ,env ))))) ’(lambda ( 0 ) (list 0 (list ’quote 0 ))))
(6≡ (( 0 closure)) (( 0 list)) (( 0 quote)))
(define rator? (sym 0 )))
(let ((op-names ’(lambda quote list)))
(lambda (x env ) Sure enough, this is our old friend, quinec .
(not (and (symbol? x ) We can push things further by attempting to generate
(memq x op-names) twines, also known as “twin quines” or “double quines.”
(not-in-env? x env )))))) That is, we want to find programs p and q such that (eval p)
⇒ q and (eval q) ⇒ p. According to this definition every
The rator? predicate is used to ensure the procedure quine is trivially a twine, so we add the restriction that p
application clause does not overlap with the lambda, list, or and q are not equal.
quote clauses. An expression x is an operator, unless it one
of the symbols lambda, list, or quote, and it is not bound in (run1 (x )
the environment. (If x is bound in env , it means the operator (fresh (p q)
is being shadowed, and that exp is a procedure application). (6≡ p q)
The definition of eval-exp in section 3 does not need to (eval-exp o p ’() q) (eval-exp o q ’() p)
use rator? because the three λ-calculus expressions have (≡ ‘(,p ,q) x )))
different shapes: applications are represented by lists of ⇒
length two, abstractions are represented by lists of length (((’((lambda ( 0 )
three, and variables are represented by symbols. Therefore (list ’quote (list 0 (list ’quote 0 ))))
there is no overlap between clauses, which is required when ’(lambda ( 0 ) (list ’quote (list 0 (list ’quote 0 )))))
using dmatch. ((lambda ( 0 ) (list ’quote (list 0 (list ’quote 0 ))))
Here is the extended relational interpreter. ’(lambda ( 0 ) (list ’quote (list 0 (list ’quote 0 ))))))
(6≡ (( 0 closure)) (( 0 list)) (( 0 quote)))
(define eval-exp o (sym 0 )))
(lambda (exp env val ) Finally, we generate thrines: distinct programs p, q, and
(conde r such that (eval p) ⇒ q, (eval q) ⇒ r , and (eval r ) ⇒ p.
((fresh (v )
(≡ ‘(quote ,v ) exp) (run1 (x )
(not-in-env o ’quote env ) (fresh (p q r )
(absent o ’closure v ) (6≡ p q) (6≡ q r ) (6≡ r p)
(≡ v val ))) (eval-exp o p ’() q) (eval-exp o q ’() r ) (eval-exp o r ’() p)
((fresh (a∗ ) (≡ ‘(,p ,q ,r ) x )))
(≡ ‘(list . ,a∗ ) exp) ⇒
(not-in-env o ’list env ) (((”((lambda ( 0 )
(absent o ’closure a∗ ) (list ’quote (list ’quote (list 0 (list ’quote 0 )))))
(proper-list o a∗ env val ))) ’(lambda ( 0 )
((symbol o exp) (lookup o exp env val )) (list ’quote (list ’quote (list 0 (list ’quote 0 ))))))
((fresh (rator rand x body envˆ a) ’((lambda ( 0 )
(≡ ‘(,rator ,rand ) exp) (list ’quote (list ’quote (list 0 (list ’quote 0 )))))
(eval-exp o rator env ‘(closure ,x ,body ,envˆ)) ’(lambda ( 0 )
(eval-exp o rand env a) (list ’quote (list ’quote (list 0 (list ’quote 0 ))))))
(eval-exp o body ‘((,x . ,a) . ,envˆ) val ))) ((lambda ( 0 )
((fresh (x body) (list ’quote (list ’quote (list 0 (list ’quote 0 )))))
(≡ ‘(lambda (,x ) ,body) exp) ’(lambda ( 0 )
(symbol o x ) (list ’quote (list ’quote (list 0 (list ’quote 0 )))))))
(not-in-env o ’lambda env ) (6≡ (( 0 closure)) (( 0 list)) (( 0 quote)))
(≡ ‘(closure ,x ,body ,env ) val )))))) (sym 0 )))

7
6. Conclusion References
Quines have a long and interesting history: the term “quine” Claire E. Alvis, Jeremiah J. Willcock, Kyle M. Carter,
was coined by Douglas Hofstadter (1979) in honor of the William E. Byrd, and Daniel P. Friedman. cKanren:
logician Willard van Orman Quine, but the concept goes miniKanren with constraints. In Workshop on Scheme
back to Kleene’s recursion theorems (Rogers 1967). and Functional Programming, October 2011.
In section 4 we describe how the absent o constraint Krzysztof R. Apt. Principles of Constraint Programming.
can be used to distinguish general procedure application Cambridge University Press, 2003.
from uses of built-in primitives, and how this approach F. Baader and W. Snyder. Unification theory. In
correctly handles shadowing of primitives. However, there A. Robinson and A. Voronkov, editors, Handbook of Au-
are other ways to distinguish between application and uses tomated Reasoning, volume I, chapter 8, pages 445–532.
of primitives. Our first efforts involved tagging procedure Elsevier Science, 2001. URL citeseer.ist.psu.edu/
applications—that is, the Scheme expression (e1 e2 ) would baader99unification.html.
be written in the interpreted language as (app e1 e2 ). Al-
though this works, it is problematic in that generated pro- Hendrik Pieter Barendregt. The Lambda Calculus – Its
grams are not quite Scheme programs. The tagging of appli- Syntax and Semantics, volume 103 of Studies in Logic and
cation is especially problematic in the presence of quote and the Foundations of Mathematics. North-Holland, 1984.
becomes most obvious when attempting to generate and in- Leo Broukhis, Simon Cooper, and Landon Curt Noll. The
terpret quines. A special “unparser” could be used to remove International Obfuscated C Code Contest. http://www.
the app tags, making the answers readable. The tagless ap- ioccc.org/.
proach, however, allows the results of running the interpreter William E. Byrd. Relational Programming in miniKanren:
backwards to be pasted directly into the Scheme REPL and Techniques, Applications, and Implementations. PhD the-
run without modification, while also allowing built-in forms sis, Indiana University, 2009.
to be shadowed. William E. Byrd and Daniel P. Friedman. From variadic
functions to variadic relations: A miniKanren perspective.
In Robby Findler, editor, Proceedings of the 2006 Scheme
Acknowledgments and Functional Programming Workshop, University of
Stuart Halloway asked if an earlier version of our relational Chicago Technical Report TR-2006-06, pages 105–117,
interpreter could generate quines. His thirty-second question 2006.
inspired the work described in this paper and resulted in William E. Byrd and Daniel P. Friedman. αKanren: A fresh
significant improvements to miniKanren. We thank Stuart name in nominal logic programming. In Proceedings of the
for his question, and look forward to his next challenge. 2007 Workshop on Scheme and Functional Programming,
Many students in the Indiana University pl-wonks group Universite Laval Technical Report DIUL-RT-0701, pages
joined us for an advanced programming languages course 79–90 (see also http://www.cs.indiana.edu/~webyrd
the semester after Stuart asked his question; one of the for improvements), 2007.
main topics of the course was running interpreters back- Edsger W. Dijkstra. Guarded commands, nondeterminacy
wards. That group of students deserves our appreciation and and formal derivation of programs. Commun. ACM, 18
thanks both for their wisdom and enthusiasm. Among that (8):453–457, August 1975.
group was Claire Alvis, who was instrumental in implement-
ing our constraint system cKanren, which allowed everyone Daniel P. Friedman, William E. Byrd, and Oleg Kiselyov.
in this course to build backward-running interpreters. She, The Reasoned Schemer. The MIT Press, Cambridge, MA,
too, deserves much credit. We thank Jason Hemann, Aaron 2005.
Todd, and Cameron Swords for their involvement in devel- Ralf Hinze. Deriving backtracking monad transformers. In
oping software (some of which found its way into this paper) Proceedings of the Fifth ACM SIGPLAN International
and their generally helpful comments. Jason also helped Dan Conference on Functional Programming, ICFP ’00, Mon-
with LATEX and revision control issues, and was instrumental treal, Canada, September 18–21, 2000, pages 186–197.
in improving appendix D. ACM Press, 2000.
None of this would have been possible without the incred- Douglas R. Hofstadter. Gödel, Escher, Bach : an eternal
ibly useful and timely observations of Mitchell Wand and golden braid. Basic, 1979.
Steve Ganz. Oleg Kiselyov joined this effort early on and Oleg Kiselyov, William E. Byrd, Daniel P. Friedman, and
he has been a constant rudder, keeping us grounded to the Chung-chieh Shan. Pure, declarative, and construc-
mathematics of logic programming. Everything in miniKan- tive arithmetic relations (declarative pearl). In Jacques
ren has been influenced by the ideas of Oleg. Please accept Garrigue and Manuel Hermenegildo, editors, Proceedings
our thanks for all your help. Chung-chieh Shan offered to re- of the 9th International Symposium on Functional and
vise our implementation of miniKanren, which first appeared Logic Programming, volume 4989 of LNCS, pages 64–80.
in the The Reasoned Schemer. Our later implementations, Springer, 2008.
including cKanren, αKanren, and this newer miniKanren, David B. MacQueen, Philip Wadler, and Walid Taha. How
have barely veered away from Chung-chieh’s masterful code. to add laziness to a strict language without even being
We appreciate and thank him for this extraordinarily elegant odd. In Proceedings of the 1998 ACM Workshop on ML,
code. As always, we thank Dorai Sitaram for SLATEX. We pages 24–30, September 1998. Baltimore, MD.
also thank Ramana Kumar and the anonymous reviewers
for their comments. Eugenio Moggi. Notions of computation and monads. In-
Working on a long-lived project, it is always difficult to formation and Computation, 93(1):55–92, 1991.
recall all those we want to thank, but hopefully between the Chris Okasaki. Purely functional data structures. Cambridge
acknowledgments in our other papers and book we have not University Press, 1999.
missed anyone.

8
Hartley Rogers, Jr. Theory of recursive functions and effec- to other goals to handle these primitives. The goals to handle
tive computability. McGraw-Hill, New York, NY, 1967. sub1 , zero? , ∗, cons, car , cdr , not, and if, rely on one or
Gary P. Thompson II. The quine page (self-reproducing more mutually-recursive calls to eval-exp o .
code). http://www.nyx.org/~gthompso/quine.htm. (define prim-exp o
Philip Wadler. How to replace failure by a list of successes: (lambda (exp env val )
A method for exception handling, backtracking, and pat- (conde
tern matching in lazy functional languages. In Jean- ((boolean-prim o exp env val ))
Pierre Jouannaud, editor, Proceedings of the Second Con- ((number-prim o exp env val ))
ference on Functional Programming Languages and Com- ((sub1-prim o exp env val ))
puter Architecture, volume 201 of Lecture Notes in Com- ((zero?-prim o exp env val ))
puter Science, pages 113–128, Nancy, France, Septem- ((*-prim o exp env val ))
ber 16–19, 1985. Springer-Verlag. ((cons-prim o exp env val ))
Philip Wadler. The essence of functional programming. In ((car-prim o exp env val ))
Conference Record of the Nineteenth ACM SIGPLAN- ((cdr-prim o exp env val ))
SIGACT Symposium on Principles of Programming Lan- ((not-prim o exp env val ))
guages, pages 1–14, Albuquerque, New Mexico, January, ((if-prim o exp env val )))))
1992. ACM Press. (define boolean-prim o
(lambda (exp env val )
A. An Extended Interpreter (conde
((≡ #t exp) (≡ #t val ))
Here we present a fully relational interpreter for an uncurried
((≡ #f exp) (≡ #f val )))))
Scheme with arithmetic operators, conditionals, and pairs;
this interpreter generates quines more slowly than the one (define number-prim o
in section 5, due to the higher branching factor. (lambda (exp env val )
Instead of using Scheme numbers, eval-exp o uses the (fresh (n)
relational arithmetic system described in appendix B. (≡ ‘(int-exp ,n) exp)
(define eval-exp o (≡ ‘(int-val ,n) val )
(lambda (exp env val ) (not-in-env o ’int-exp env ))))
(conde (define sub1-prim o
((fresh (v ) (lambda (exp env val )
(≡ ‘(quote ,v ) exp) (fresh (e n n-1 )
(not-in-env o ’quote env ) (≡ ‘(sub1 ,e) exp)
(absent o ’closure v ) (≡ ‘(int-val ,n-1 ) val )
(absent o ’int-val v ) (not-in-env o ’sub1 env )
(≡ v val ))) (eval-exp o e env ‘(int-val ,n))
((fresh (a∗ ) (−o n ’(1) n-1 ))))
(≡ ‘(list . ,a∗ ) exp)
(not-in-env o ’list env ) (define zero?-prim o
(absent o ’closure a∗ ) (lambda (exp env val )
(absent o ’int-val a∗ ) (fresh (e n)
(proper-list o a∗ env val ))) (≡ ‘(zero? ,e) exp)
((prim-exp o exp env val )) (conde
((symbol o exp) (lookup o exp env val )) ((zero o n) (≡ #t val ))
((fresh (rator x∗ rands body env2 a∗ res) ((pos o n) (≡ #f val )))
(≡ ‘(,rator . ,rands) exp) (not-in-env o ’zero? env )
(eval-exp o rator env ‘(closure ,x∗ ,body ,env2 )) (eval-exp o e env ‘(int-val ,n)))))
(proper-list o rands env a∗ ) (define *-prim o
(ext-env ∗o x∗ a∗ env2 res) (lambda (exp env val )
(eval-exp o body res val ))) (fresh (e1 e2 n1 n2 n3 )
((fresh (x∗ body) (≡ ‘(∗ ,e1 ,e2 ) exp)
(≡ ‘(lambda ,x∗ ,body) exp) (≡ ‘(int-val ,n3 ) val )
(not-in-env o ’lambda env ) (not-in-env o ’∗ env )
(≡ ‘(closure ,x∗ ,body ,env ) val )))))) (eval-exp o e1 env ‘(int-val ,n1 ))
(define ext-env ∗o (eval-exp o e2 env ‘(int-val ,n2 ))
(lambda (x∗ a∗ env out) (∗o n1 n2 n3 ))))
(conde (define cons-prim o
((≡ ’() x∗ ) (≡ ’() a∗ ) (≡ env out)) (lambda (exp env val )
((fresh (x a dx∗ da∗ env2 ) (fresh (a d v-a v-d )
(≡ ‘(,x . ,dx∗) x∗ ) (≡ ‘(cons ,a ,d ) exp)
(≡ ‘(,a . ,da∗) a∗ ) (≡ ‘(,v-a . ,v-d ) val )
(≡ ‘((,x . ,a) . ,env ) env2 ) (absent o ’closure val )
(ext-env ∗o dx∗ da∗ env2 out)))))) (absent o ’int-val val )
Primitive expressions include boolean literals, numbers (not-in-env o ’cons env )
(represented as tagged little-endian lists of bits), pairs, and (eval-exp o a env v-a)
operations over these values. The goal prim-exp o dispatches (eval-exp o d env v-d ))))

9
(define car-prim o (sub1 (sub1 (sub1 (int-exp (1 0 0 1)))))
(lambda (exp env val )
(fresh (p d ) is the 270th value.
(≡ ‘(car ,p) exp) Next, we calculate the factorial of five, using “The Poor-
(6≡ ’int-val val ) man’s Y Combinator.”
(6≡ ’closure val ) (define rel-fact5
(not-in-env o ’car env ) ‘((lambda (f)
(eval-exp o p env ‘(,val . ,d ))))) ((f f) (int-exp ,(build-num 5))))
(lambda (f)
(define cdr-prim o (lambda (n)
(lambda (exp env val ) (if (zero? n)
(fresh (p a) (int-exp ,(build-num 1))
(≡ ‘(cdr ,p) exp) (∗ n ((f f) (sub1 n))))))))
(6≡ ’int-val a)
(6≡ ’closure a) (run∗ (q) (eval-exp o rel-fact5 ’() q))
(not-in-env o ’cdr env ) ⇒ ((int-val (0 0 0 1 1 1 1)))
(eval-exp o p env ‘(,a . ,val )))))
Now that we know our interpreter works, we are ready
(define not-prim o to generate quines in our extended language:
(lambda (exp env val ) (run5 (q) (eval-exp o q ’() q))
(fresh (e b) ⇒
(≡ ‘(not ,e) exp) (#t
(conde #f
((≡ #t b) (≡ #f val )) (((lambda ( 0 ) (list 0 (list ’quote 0 )))
((≡ #f b) (≡ #t val ))) ’(lambda ( 0 ) (list 0 (list ’quote 0 ))))
(not-in-env o ’not env ) (6≡ (( 0 closure))
(eval-exp o e env b)))) (( 0 int-val))
(define if-prim o (( 0 list))
(lambda (exp env val ) (( 0 quote)))
(fresh (e1 e2 e3 t) (sym 0 ))
(≡ ‘(if ,e1 ,e2 ,e3 ) exp) (((lambda ( 0 ) (list 0 (list (car ’(quote . 1 )) 0 )))
(not-in-env o ’if env ) ’(lambda ( 0 ) (list 0 (list (car ’(quote . 1 )) 0 ))))
(eval-exp o e1 env t) (6≡ (( 0 car))
(conde (( 0 closure))
((≡ #t t) (eval-exp o e2 env val )) (( 0 int-val))
((≡ #f t) (eval-exp o e3 env val )))))) (( 0 list))
(( 0 quote)))
Now we can consider several examples using eval-exp o . (absent closure 1 )
Consider this run expression, which returns 12 expressions (absent int-val 1 )
that evaluate to six in the empty environment. (sym 0 ))
(run12 (q) (eval-exp o q ’() ‘(int-val ,(build-num 6)))) (((lambda ( 0 ) (list (list ’lambda ’( 0 ) 0 ) (list ’quote 0 )))
⇒ ’(list (list ’lambda ’( 0 ) 0 ) (list ’quote 0 )))
((int-exp (0 1 1)) (6≡ (( 0 closure))
((lambda () (int-exp (0 1 1)))) (( 0 int-val))
(sub1 (int-exp (1 1 1))) (( 0 list))
(((lambda ( 0 ) (int-exp (0 1 1))) ’ 1 ) (( 0 quote)))
(6≡ (( 0 int-exp))) (sym 0 )))
(absent closure 1 )
(absent int-val 1 )) Not surprisingly, booleans are quines, since they are self-
(∗ (int-exp (1)) (int-exp (0 1 1))) evaluating literals. The other answers are more interesting—
(∗ (int-exp (0 1 1)) (int-exp (1))) we encourage the reader to look for patterns in the answers.
(∗ (int-exp (0 1)) (int-exp (1 1)))
(((lambda ( 0 ) (int-exp (0 1 1))) (list)) B. A Relational Arithmetic System
(6≡ (( 0 int-exp)))) To make the paper self-contained, we present the relational
(car (list (int-exp (0 1 1)))) arithmetic system used in the extended interpreter of ap-
((lambda () ((lambda () (int-exp (0 1 1)))))) pendix A. Variants of this arithmetic system have been de-
(sub1 ((lambda () (int-exp (1 1 1))))) scribed in Kiselyov et al. (2008) (with termination proofs for
((lambda () (sub1 (int-exp (1 1 1)))))) the individual operators), Byrd (2009), and Friedman et al.
The 7th value in this list is (2005)—please see these references for a detailed description
of the code.
(∗ (int-exp (0 1)) (int-exp (1 1))) A note on typography: +o is entered as pluso, −o as
minuso, ∗o as *o, and ÷o as /o.
And, if we look at the first 500 answers,
B.1 Relational Arithmetic
(run500 (q) (eval-exp o q ’() ‘(int-val ,(build-num 6))))
Relational arithmetic allows for queries such as ‘what are five
we discover triples of natural numbers x, y, and z for which x + y = z?’,
and ‘for which natural numbers x and y does x · y = 24
hold?’, which can be expressed in miniKanren as
10
(run5 (q) (define build-num
(fresh (x y z ) (lambda (n)
(+o x y z ) (cond
(≡ ‘(,x ,y ,z ) q))) ((odd? n)
and (cons 1
(build-num (÷ (− n 1) 2))))
(run∗ (q) ((and (not (zero? n)) (even? n))
(fresh (x y) (cons 0
(∗o x y (build-num 24)) (build-num (÷ n 2))))
(≡ ‘(,x ,y ,(build-num 24)) q))) ((zero? n) ’()))))
respectively.
In order to understand the answers to these runs, it (define zero o
is necessary to know how we represent numbers. Ground (lambda (n)
numbers are represented in “little endian” style using lists (≡ ’() n)))
of bits. The most significant bit in the list cannot be 0; this (define pos o
restriction ensures each number has a unique representation. (lambda (n)
Zero is therefore represented by the empty list rather than (fresh (a d )
(0), to avoid violating this restriction. The number one is (≡ ‘(,a . ,d ) n))))
represented by (1), the number two by (0 1), etc.
A number need not be ground, so long as it is not (define >1o
instantiated to a list ending with 0. For example, ‘(1 . ,x ) (lambda (n)
represents any odd natural number, while ‘(0 . ,x ) represents (fresh (a ad dd )
any positive even number (with the restriction that x must (≡ ‘(,a ,ad . ,dd ) n))))
represent a positive integer, which we shall assume in the
rest of this description). The list (0 0 0 1) represents the (define full-adder o
number 8, while ‘(0 0 0 . ,x ) represents multiples of 8. If x (lambda (b x y r c)
is (1), the multiple is just 8. If x is (0 1), the multiple of 8 is (conde
16, and so forth. Numbers can be even more sophisticated: ((≡ 0 b) (≡ 0 x) (≡ 0 y) (≡ 0 r) (≡ 0 c))
‘(0 ,y 0 . ,x ) represents multiples of 8 if y is 0, and numbers ((≡ 1 b) (≡ 0 x) (≡ 0 y) (≡ 1 r) (≡ 0 c))
of the form 8x + 2 if y is 1. ((≡ 0 b) (≡ 1 x) (≡ 0 y) (≡ 1 r) (≡ 0 c))
Here are the answers to the run5 expression above. The ((≡ 1 b) (≡ 1 x) (≡ 0 y) (≡ 0 r) (≡ 1 c))
first answer states that for x ≥ 0, x + 0 = x; the second ((≡ 0 b) (≡ 0 x) (≡ 1 y) (≡ 1 r) (≡ 0 c))
answer states that for x > 0, 0 + x = x; the third answer ((≡ 1 b) (≡ 0 x) (≡ 1 y) (≡ 0 r) (≡ 1 c))
states that 1 + 1 = 2; the fourth answer states that for x > 0 ((≡ 0 b) (≡ 1 x) (≡ 1 y) (≡ 0 r) (≡ 1 c))
and y ≤ 1, 1 + (4x + y) = 4x + y + 1; and the fifth answer ((≡ 1 b) (≡ 1 x) (≡ 1 y) (≡ 1 r) (≡ 1 c)))))
states that 1 + 3 = 4.
(define adder o
(( 0 () 0 ) (lambda (d n m r )
(() ( 0 . 1 ) ( 0 . 1 )) (conde
((1) (1) (0 1)) ((≡ 0 d ) (≡ ’() m) (≡ n r ))
((1) (0 0 . 1 ) (1 0 . 1 )) ((≡ 0 d ) (≡ ’() n) (≡ m r )
((1) (1 1) (0 0 1))) (pos o m))
((≡ 1 d ) (≡ ’() m)
And here are the answers to the run∗ expression above.
(adder o 0 n ’(1) r ))
There are eight answers, each one producing a different way
((≡ 1 d ) (≡ ’() n) (pos o m)
to multiply two numbers to yield 24. For example, the fifth
(adder o 0 ’(1) m r ))
answer states that 8 times 3 is 24.
((≡ ’(1) n) (≡ ’(1) m)
(((1) (0 0 0 1 1) (0 0 0 1 1)) (fresh (a c)
((0 0 0 1 1) (1) (0 0 0 1 1)) (≡ ‘(,a ,c) r )
((0 1) (0 0 1 1) (0 0 0 1 1)) (full-adder o d 1 1 a c)))
((0 0 1) (0 1 1) (0 0 0 1 1)) ((≡ ’(1) n) (gen-adder o d n m r ))
((0 0 0 1) (1 1) (0 0 0 1 1)) ((≡ ’(1) m) (>1o n) (>1o r )
((1 1) (0 0 0 1) (0 0 0 1 1)) (adder o d ’(1) n r ))
((0 1 1) (0 0 1) (0 0 0 1 1)) ((>1o n) (gen-adder o d n m r )))))
((0 0 1 1) (0 1) (0 0 0 1 1)))
(define gen-adder o
Our system includes other relational arithmetic opera- (lambda (d n m r )
tors: subtraction (−o ), integer division with remainder (÷o ), (fresh (a b c e x y z )
integer logarithm with remainder (log o ), and exponentiation (≡ ‘(,a . ,x ) n)
(expo , which is derived from log o ). (≡ ‘(,b . ,y) m) (pos o y)
(≡ ‘(,c . ,z ) r ) (pos o z )
B.2 Core Arithmetic Operators
(full-adder o d a b c e)
This subsection contains arithmetic operators used in the (adder o e x y z ))))
extended interpreter in appendix A.
(define +o (lambda (n m k ) (adder o 0 n m k )))
(define −o (lambda (n m k ) (+o m k n)))

11
(define ∗o (define <o
(lambda (n m p) (lambda (n m)
(conde (conde
((≡ ’() n) (≡ ’() p)) ((<l o n m))
((pos o n) (≡ ’() m) (≡ ’() p)) ((=l o n m)
((≡ ’(1) n) (pos o m) (≡ m p)) (fresh (x )
((>1o n) (≡ ’(1) m) (≡ n p)) (pos o x )
((fresh (x z ) (+o n x m))))))
(≡ ‘(0 . ,x ) n) (pos o x )
(≡ ‘(0 . ,z ) p) (pos o z ) (define 6o
(>1o m) (lambda (n m)
(∗o x m z ))) (conde
((fresh (x y) ((≡ n m))
(≡ ‘(1 . ,x ) n) (pos o x ) ((<o n m)))))
(≡ ‘(0 . ,y) m) (pos o y) (define ÷o
(∗o m n p))) (lambda (n m q r )
((fresh (x y) (conde
(≡ ‘(1 . ,x ) n) (pos o x ) ((≡ r n) (≡ ’() q) (<o n m))
(≡ ‘(1 . ,y) m) (pos o y) ((≡ ’(1) q) (=l o n m) (+o r m n) (<o r m))
(odd-∗o x n m p)))))) ((<l o m n) (<o r m) (pos o q)
(define odd-∗o (fresh (nh nl qh ql qlm qlmr rr rh )
(lambda (x n m p) (split o n r nl nh )
(fresh (q) (split o q r ql qh )
(bound-∗o q p n m) (conde
(∗o x m q) ((≡ ’() nh ) (≡ ’() qh )
(+o ‘(0 . ,q) m p)))) (−o nl r qlm)
(∗o ql m qlm))
(define bound-∗o ((pos o nh )
(lambda (q p n m) (∗o ql m qlm)
(conde (+o qlm r qlmr )
((≡ ’() q) (pos o p)) (−o qlmr nl rr )
((fresh (a0 a1 a2 a3 x y z ) (split o rr r ’() rh )
(≡ ‘(,a0 . ,x ) q) (÷o nh m qh rh ))))))))
(≡ ‘(,a1 . ,y) p)
(conde (define split o
((≡ ’() n) (≡ ‘(,a2 . ,z ) m) (lambda (n r l h)
(bound-∗o x y z ’())) (conde
((≡ ‘(,a3 . ,z ) n) (bound-∗o x y z m)))))))) ((≡ ’() n) (≡ ’() h) (≡ ’() l ))
((fresh (b n̂)
B.3 Additional Arithmetic Operators (≡ ‘(0 ,b . ,n̂) n)
This subsection contains useful arithmetic operators, beyond (≡ ’() r )
those used in the extended interpreter in appendix A. (≡ ‘(,b . ,n̂) h)
(≡ ’() l )))
(define =l o
((fresh (n̂)
(lambda (n m)
(≡ ‘(1 . ,n̂) n)
(conde
(≡ ’() r )
((≡ ’() n) (≡ ’() m))
(≡ n̂ h)
((≡ ’(1) n) (≡ ’(1) m))
(≡ ’(1) l )))
((fresh (a x b y)
((fresh (b n̂ a r̂)
(≡ ‘(,a . ,x ) n) (pos o x )
(≡ ‘(0 ,b . ,n̂) n)
(≡ ‘(,b . ,y) m) (pos o y)
(≡ ‘(,a . ,r̂) r )
(=l o x y))))))
(≡ ’() l )
(define <l o (split o ‘(,b . ,n̂) r̂ ’() h)))
(lambda (n m) ((fresh (n̂ a r̂)
(conde (≡ ‘(1 . ,n̂) n)
((≡ ’() n) (pos o m)) (≡ ‘(,a . ,r̂) r )
((≡ ’(1) n) (>1o m)) (≡ ’(1) l )
((fresh (a x b y) (split o n̂ r̂ ’() h)))
(≡ ‘(,a . ,x ) n) (pos o x ) ((fresh (b n̂ a r̂ ˆ l)
(≡ ‘(,b . ,y) m) (pos o y) (≡ ‘(,b . ,n̂) n)
(<l o x y)))))) (≡ ‘(,a . ,r̂) r )
(define 6l o (≡ ‘(,b . ,ˆ l) l )
(lambda (n m) (pos o ˆl)
(conde (split o n̂ r̂ ˆ
l h))))))
((=l o n m))
((<l o n m)))))

12
(define log o (define repeated-mul o
(lambda (n b q r ) (lambda (n q nq)
(conde (conde
((≡ ’(1) n) (pos o b) (≡ ’() q) (≡ ’() r )) ((pos o n) (≡ ’() q) (≡ ’(1) nq))
((≡ ’() q) (<o n b) (+o r ’(1) n)) ((≡ ’(1) q) (≡ n nq))
((≡ ’(1) q) (>1o b) (=l o n b) (+o r b n)) ((>1o q)
((≡ ’(1) b) (pos o q) (+o r ’(1) n)) (fresh (q1 nq1 )
((≡ ’() b) (pos o q) (≡ r n)) (+o q1 ’(1) q)
((≡ ’(0 1) b) (repeated-mul o n q1 nq1 )
(fresh (a ad dd ) (∗o nq1 n nq))))))
(pos o dd )
(define expo
(≡ ‘(,a ,ad . ,dd ) n)
(lambda (b q n)
(exp2 o n ’() q)
(log o n b q ’())))
(fresh (s)
(split o n dd r s))))
((fresh (a ad add ddd ) C. Generalized Pattern Matcher
(conde This appendix describes and defines the dmatch pat-
((≡ ’(1 1) b)) tern matcher, which is a generalization of Oleg Kiselyov’s
((≡ ‘(,a ,ad ,add . ,ddd ) b)))) pmatch that appeared in Byrd and Friedman (2007).
(<l o b n) dmatch improves error reporting, since now it is possible to
(fresh (bw1 bw nw nw1 ql1 ql s) associate a string with each use of pattern matching, as with
(exp2 o b ’() bw1 ) the name "example" in the definition of h below. dmatch
(+o bw1 ’(1) bw ) does not handle quote specially, which allows for certain
(<l o q n) common patterns to be specified that were previously not
(fresh (q1 bwq1 ) possible. Finally, dmatch does not support the else aux-
(+o q ’(1) q1 ) iliary keyword, and the order of the clauses is arbitrary—
(∗o bw q1 bwq1 ) however, only one pattern (plus guard) can succeed for each
(<o nw1 bwq1 )) invocation of dmatch. Here is an example of dmatch.
(exp2 o n ’() nw1 ) (define h
(+o nw1 ’(1) nw ) (lambda (x y)
(÷o nw bw ql1 s) (dmatch ‘(,x . ,y) "example"
(+o ql ’(1) ql1 ) ((,a . ,b)
(6l o ql q) (guard (number? a) (number? b))
(fresh (bql qh s qdh qd ) (∗ a b))
(repeated-mul o b ql bql ) ((,a ,b ,c)
(÷o nw bw1 qh s) (guard (number? a) (number? b) (number? c))
(+o ql qdh qh ) (+ a b c)))))
(+o ql qd q)
(6o qd qdh) (list (h 3 4) (apply h ‘(1 (3 4)))) ⇒ (12 8)
(fresh (bqd bq1 bq)
(repeated-mul o b qd bqd ) In this example, a dotted pair is matched against two dif-
(∗o bql bqd bq) ferent patterns. In the first clause, the value of x is lexi-
(∗o b bq bq1 ) cally bound to a and the value of y is lexically bound to
(+o bq r n) b. Before the pattern match succeeds, however, an optional
(<o n bq1 )))))))) side-effect-free guard is run within the scope of a and b. The
guard succeeds only if a and b are bound to numbers; if so,
(define exp2 o then their product is returned. The second clause attempts
(lambda (n b q) to match the dotted pair against a three-element list, once
(conde again with an optional guard. If the values bound to a, b,
((≡ ’(1) n) (≡ ’() q)) and c are all numbers, the second clause returns their sum.
((>1o n) (≡ ’(1) q) Here is the grammar for dmatch, where exp is any
(fresh (s) pure Scheme expression, boolean-exp is any pure Scheme
(split o n b s ’(1)))) predicate expression, var is any valid Scheme identifier,
((fresh (q1 b2 ) literal is any Scheme literal, and name-string is any literal
(≡ ‘(0 . ,q1 ) q) Scheme string:
(pos o q1 )
(<l o b n)
(append o b ‘(1 . ,b) b2 ) match := (dmatch exp {name-string} clause . . .)
(exp2 o n b2 q1 ))) clause := (pattern {guard} exp . . .)
((fresh (q1 nh b2 s) guard := (guard boolean-exp . . .)
(≡ ‘(1 . ,q1 ) q)
(pos o q1 ) pattern := , var
(pos o nh ) | literal
(split o n b s nh ) | (pattern1 pattern2 . . .)
(append o b ‘(1 . ,b) b2 )
(exp2 o nh b2 q1 )))))) | (pattern1 . pattern2 )

13
Now we examine the implementation of dmatch. The main (define-syntax ppat
dmatch macro simply handles the optional name string, (syntax-rules (unquote)
and passes off control to the auxiliary helpers. The auxiliary (( v (unquote var) kt kf ) (let ((var v )) kt))
macros will produce a list of “packages,” which is then (( v (x . y) kt kf )
processed by the run-a-thunk procedure. (if (pair? v )
(define-syntax dmatch (let ((vx (car v )) (vy (cdr v )))
(syntax-rules () (ppat vx x (ppat vy y kt kf ) kf ))
(( v (e . . . ) . . . ) kf ))
(let ((pkg∗ (dmatch-remexp v (e . . . ) . . . ))) (( v lit kt kf ) (if (equal? v (quote lit)) kt kf ))))
(run-a-thunk ’v v #f pkg∗))) If there is no match, the error is reported by no-matching-
(( v name (e . . . ) . . . ) pattern (using the non-standard printf function). If there
(let ((pkg∗ (dmatch-remexp v (e . . . ) . . . ))) is an overlap between two or more patterns/guards, then
(run-a-thunk ’v v ’name pkg∗))))) overlapping-patterns/guards signals an error. Otherwise, if
A package comprises a clause and a thunk, and is con- there is no overlap, the thunk in the singleton package list
structed/destructed using these functions: is invoked.
(define pkg (lambda (cls thk ) (cons cls thk ))) (define run-a-thunk
(define pkg-clause (lambda (pkg) (car pkg))) (lambda (v-expr v name pkg∗)
(define pkg-thunk (lambda (pkg) (cdr pkg))) (cond
((null? pkg∗) (no-matching-pattern name v-expr v ))
dmatch-remexp ensures that the input expression to ((null? (cdr pkg∗)) ((pkg-thunk (car pkg∗))))
dmatch is evaluated only once. (else
(define-syntax dmatch-remexp (ambiguous-pattern/guard name v-expr v pkg∗)))))
(syntax-rules ()
(( (rator rand . . . ) cls . . . ) (define no-matching-pattern
(let ((v (rator rand . . . ))) (lambda (name v-expr v )
(dmatch-aux v cls . . . ))) (if name
(( v cls . . . ) (dmatch-aux v cls . . . )))) (printf "dmatch ˜d failed˜n˜d ˜d˜n"
Each expansion of dmatch-aux creates a package list of name v-expr v )
some type. There are three cases: two recursive cases and a (printf "dmatch failed˜n˜d ˜d˜n"
single base case. If a pattern without a guard matches the v-expr v ))
input, that clause and its thunk are added to the package (error ’dmatch "match failed")))
list. If a matching pattern has a guard, the clause and thunk (define overlapping-patterns/guards
are added to the package list only if the guard also succeeds. (lambda (name v-expr v pkg∗)
(define-syntax dmatch-aux (if name
(syntax-rules (guard) (printf "dmatch ˜d overlapping matching clauses˜n"
(( v ) ’()) name)
(( v (pat (guard g . . . ) e0 e . . . ) cs . . . ) (printf "dmatch overlapping matching clauses˜n"))
(let ((fk (lambda () (dmatch-aux v cs . . . )))) (printf "with ˜d evaluating to ˜d˜n" v-expr v )
(ppat v pat (printf " ˜n")
(if (not (and g . . . )) (for-each pretty-print (map pkg-clause pkg∗))))
(fk )
(cons (pkg ’(pat (guard g . . . ) e0 e . . . ) Here is the definition of h (eliding the second clause) after
(lambda () e0 e . . . )) macro expansion.
(fk ))) (lambda (x y)
(fk )))) (let ((pkg∗
(( v (pat e0 e . . . ) cs . . . ) (let ((v (cons x y)))
(let ((fk (lambda () (dmatch-aux v cs . . . )))) (let ((fk (lambda () . . .)))
(ppat v pat (if (pair? v )
(cons (pkg ’(pat e0 e . . . ) (let ((vx (car v )) (vy (cdr v )))
(lambda () e0 e . . . )) (let ((a vx ))
(fk )) (let ((b vy))
(fk )))))) (if (not (if (number? a) (number? b) #f))
The ppat helper macro does the actual pattern matching, (fk )
then expands into one of two forms. The consequent ex- (cons
pression is the result of the expansion of ppat if the pattern (pkg
matches, and the alternate expression otherwise. In all cases, ’((,a . ,b)
the alternate is just another dmatch-aux macro that drops (guard
the first pattern and continues the recursive expansion. The (number? a)
alternative is encoded as a thunk, to avoid expanding the (number? b))
same expression multiple times. (∗ a b))
ppat leverages the syntax-rules pattern matcher to do (lambda () (∗ a b)))
most of the work. The pair case performs tree recursion to (fk ))))))
match against the car and cdr . The last clause uses equal? (fk ))))))
rather than eq? in order to handle vectors and other data. (run-a-thunk ’‘(,x . ,y) (cons x y) "example" pkg∗)))

14
There are two kinds of improvements that should be resolved (define-syntax λF
by the compiler. First, vx and vy are not needed, so they (syntax-rules () (( () e) (lambda () e))))
should not get bindings. The lexical variables a and b could
have replaced vx and vy, respectively. Second, a and b (define-syntax inc
should be parallel let bindings. (syntax-rules () (( e) (λF () e))))

(define empty-f (λF () (mzero)))

D. miniKanren Implementation
A singleton stream c is the same as (choice c empty-f ). For
Our miniKanren implementation comprises two kinds of goals that return only a single package, however, using this
operators: the interface operators run and run∗ ; and goal special representation of a singleton stream avoids the cost of
constructors ≡, 6≡, symbol o , number o , absent o , conde , and unnecessarily building and taking apart pairs, and creating
fresh, which take a package implicitly. and invoking thunks.
A package is a list of four values, each of which is, or To ensure that the values produced by these four kinds
contains, an association list of variables to values. The first of c∞ ’s can be distinguished, we assume that a package is
value in a package is a substitution, S . The second value in never #f, a function, or a pair whose cdr is a function. To
a package is a list of association lists, D; each association discriminate among these four cases, we define case∞ .
list, d , represents a disequality constraint. The third value in
a package is an association list, A, that associates a variable (define-syntax case∞
with a pair consisting of a tag and a predicate. If a variable, (syntax-rules ()
say x , is associated with the tag sym, then we know that (( e (() e0 ) ((fˆ) e1 ) ((ĉ) e2 ) ((c f ) e3 ))
x may only be associated in the substitution with either a (let ((c∞ e))
fresh variable or a symbol. Any attempt to associate x with (cond
any other kind of value leads to failure. A has within it ((not c∞ ) e0 )
constraints that are used to support symbol o and number o . ((procedure? c∞ ) (let ((fˆ c∞ )) e1 ))
The final value in a package is also an association list, T , ((not (and (pair? c∞ )
whose members associate a variable with a pair consisting (procedure? (cdr c∞ ))))
of a tag and a predicate. T has within it constraints that (let ((ĉ c∞ )) e2 ))
are used to support absent o . (else (let ((c (car c∞ )) (f (cdr c∞ )))
(define c
S (lambda (c) (car c))) e3 )))))))
(define c
D (lambda (c) (cadr c))) To get answers from the potentially infinite stream, we
(define c
A (lambda (c) (caddr c))) use the run interface. The interface operator run uses take
(define c
T (lambda (c) (cadddr c))) to convert an f to an even stream (MacQueen et al. 1998).
(define empty-c ’(() () () ())) The definition of run places an artificial goal at the tail
A goal g is a function that maps a package c to an ordered of g0 g . . . This artificial goal invokes reify (section 2.1) on
sequence c∞ of zero or more packages. (For clarity, we notate the variable x using the final package final-c produced by
lambda as λG when creating such a function g.) running all the goals in the empty package empty-c.
(define-syntax λG (define-syntax run
(syntax-rules (:) (syntax-rules ()
(( (c) e) (lambda (c) e)) (( n (x ) g0 g . . . )
(( (c : S D A T ) e) (take n
(lambda (c) (λF ()
(let ((S (c
S c)) ((fresh (x ) g0 g . . .
(D (c
D c)) (λG (final-c)
(A (c
A c)) (let ((z ((reify x ) final-c)))
(T (c
T c))) (choice z empty-f ))))
e))))) empty-c))))))
Because a sequence of packages may be infinite, we rep-
resent it not as a list but as a c∞ , a special kind of stream (define-syntax run∗
that can contain either precisely zero, precisely one, or one (syntax-rules ()
or more packages (Hinze 2000; Wadler 1985). mzero, and (( (x ) g . . . ) (run #f (x ) g . . . ))))
unit, represent these first two options. We use #f to denote If the first argument to take is #f, then take returns the
the empty stream of packages. If c is a package, then c itself entire stream of reified values as a list, thereby providing the
represents the stream containing just c. behavior of run∗ . The and expressions within take detect
(define mzero (lambda () #f)) this #f case.
(define unit (λG (c) c)) (define take
(define choice (lambda (c f ) (cons c f ))) (lambda (n f )
To represent a stream containing multiple packages, we (cond
use (choice c f ), where c is the first package in the stream, ((and n (zero? n)) ’())
and where f is a thunk that, when invoked, produces the (else
remainder of the stream. (For clarity, we notate lambda (case∞ (f )
as λF when creating such a function f .) To represent an (() ’())
incomplete stream, we use (inc e), where e is an expression ((f ) (take n f ))
that evaluates to a c∞ —thus inc creates an f . ((c) (cons c ’()))
((c f ) (cons c (take (and n (− n 1)) f ))))))))

15
D.1 Goal Constructors The function make-tag-A is used to create the symbol o
To take the conjunction of goals, we define fresh, a goal and number o goal constructors and contains the essence of
constructor that first lexically binds variables built by var what those operators accomplish. Elements of A act as dae-
and then combines successive goals using bind∗ . mons. These daemons make certain that associations which
are added to the substitution do not violate A’s constraints.
(define-syntax fresh In addition, D may contain a disequality constraint between,
(syntax-rules () say, a variable y and 3; if we also know that y must be a
(( (x . . . ) g0 g . . . ) symbol, then the disequality constraint is subsumed by the
(λG (c) symbol constraint on y, and can be discarded.
(inc (let ((x (var ’x)) . . . )
(bind∗ (g0 c) g . . . ))))))) (define make-tag-A
∗ (lambda (tag pred )
bind is short-circuiting, since the empty stream is rep- (lambda (u)
resented by #f. bind∗ relies on bind (Moggi 1991; Wadler (λG (c : S D A T )
1992), which applies the goal g to each element in the stream (case-value (walk u S )
c∞ . The resulting c∞ ’s are then merged using mplus, which ((x ) (cond
combines a c∞ and an f to yield a single c∞ . ((make-tag-A+ x tag pred c S D A T )
(define-syntax bind∗ ⇒ unit)
(syntax-rules () (else (mzero))))
(( e) e) ((au du) (mzero))
(( e g0 g . . . ) (bind∗ (bind e g0 ) g . . . )))) ((u) (cond
((pred u) (unit c))
(define bind
(else (mzero)))))))))
(lambda (c∞ g)
(case∞ c∞ (define make-tag-A+
(() (mzero)) (lambda (u tag pred c S D A T )
((f ) (inc (bind (f ) g))) (cond
((c) (g c)) ((ext-A (walk u S ) tag pred S A) ⇒
((c f ) (mplus (g c) (λF () (bind (f ) g))))))) (lambda (A+)
(cond
(define mplus
((null? A+) c)
(lambda (c∞ f )
(else (let ((D (subsume A+ D))
(case∞ c∞
(A (append A+ A)))
(() (f ))
(subsume-A S D A T ))))))
((fˆ) (inc (mplus (f ) fˆ))) (else #f))))
((c) (choice c f ))
((c fˆ) (choice c (λF () (mplus (f ) fˆ))))))) (define subsume-A
To take the disjunction of goals we define conde , a (lambda (S D A T )
goal constructor that combines successive conde lines using (let ((x∗ (rem-dups (map lhs A))))
mplus∗ , which in turn relies on mplus. We use the same (subsume-A+ x∗ S D A T ))))
implicit package c for each conde line. To avoid divergence, (define subsume-A+
we treat the lines of each conde as a single inc stream. (lambda (x∗ S D A T )
(define-syntax conde (cond
(syntax-rules () ((null? x∗ ) ‘(,S ,D ,A ,T ))
(( (g0 g . . . ) (g1 ĝ . . . ) . . . ) (else (let ((x (car x∗ )))
(λG (c) (inc (mplus∗ (bind∗ (g0 c) g . . . ) (let ((D/T (update-D/T x S D A T )))
(bind∗ (g1 c) ĝ . . . ) . . . )))))) (let ((D (car D/T )) (T (cdr D/T )))
‘(,S ,D ,A ,T ))))))))
(define-syntax mplus∗
(syntax-rules () (define ext-A
(( e) e) (lambda (x tag pred S A)
(( e0 e . . . ) (mplus e0 (cond
(λF () (mplus∗ e . . . )))))) ((null? A) ‘((,x . (,tag . ,pred ))))
The pattern structure of case-value is similar to case∞ (else
in that it lists the scoped variables. If u’s value is a variable, (let ((a (car A)) (A (cdr A)))
the scope of e0 includes u’s value. If u’s value is a pair, then (let ((a-tag (pr
tag a)))
the scope of e1 includes each item in the pair. Otherwise, (cond
the scope of e2 includes the value of u. ((eq? (walk (lhs a) S ) x )
(cond
(define-syntax case-value ((tag=? a-tag tag) ’())
(syntax-rules () (else #f)))
(( u ((t1 ) e0 ) ((at dt) e1 ) ((t2 ) e2 )) (else (ext-A x tag pred S A)))))))))
(let ((t u))
(cond (define boolean o
((var? t) (let ((t1 t)) e0 )) (lambda (x )
((pair? t) (let ((at (car t)) (dt (cdr t))) e1 )) (conde
(else (let ((t2 t)) e2 ))))))) ((≡ #f x ))
((≡ #t x )))))

16
(define symbol o (make-tag-A ’sym symbol? )) Just as 6≡ checks A and T before extending D, ≡ must
o first check D, A, and T (all of which might change) before
(define number (make-tag-A ’num number? ))
succeeding.
(define pr
tag (lambda (pr ) (car (rhs pr )))) (define ≡
(define pr
pred (lambda (pr ) (cdr (rhs pr )))) (lambda (u v )
(λG (c : S D A T )
Here is the implementation of the remaining goal con- (cond
structors. The definitions of 6≡ and ≡ both use unify (sec- ((unify u v S ) ⇒
tion D.3). But, when we succeed by invoking unit, we pass (post-unify-≡ c S D A T ))
a different substitution. In the ≡ case, we pass the (possi- (else (mzero))))))
bly) extended substitution, however, in the 6≡ case, we pass
the original substitution. In the 6≡ case, the actual exten- (define post-unify-≡
sion (here called the prefix ) is a disequality constraint. We (lambda (c S D A T )
can take that constraint and make sure that A and T are (lambda (S+)
okay with each association in the prefix. Those associations (cond
that are not dropped from the prefix are added as a new ((eq? S+ S ) (unit c))
constraint to D. (There is a subtlety in the simplicity of the ((verify-D D S+) ⇒
definition of prefix-S : we know that if we keep taking cdr s (lambda (D)
starting at S+, assuming that S+ and S are not eq?, we will (cond
eventually arrive at S . This eq? is not strictly necessary, ((post-verify-D S+ D A T ) ⇒ unit)
since we are basically trying to determine if the lengths of (else (mzero)))))
the two lists are the same but more efficiently.) (else (mzero))))))
(define 6≡ (define verify-D
(lambda (u v ) (lambda (D S )
(λG (c : S D A T ) (cond
(cond ((null? D) ’())
((unify u v S ) ⇒ (post-unify-6≡ S D A T )) ((verify-D (cdr D) S ) ⇒
(else (unit c)))))) (lambda (D+)
(define post-unify-6≡ (verify-D+ (car D) D+ S )))
(lambda (S D A T ) (else #f))))
(lambda (S+) (define verify-D+
(cond (lambda (d D S )
((eq? S+ S ) (mzero)) (cond
(else (let ((D+ (list (prefix-S S+ S )))) ((unify∗ d S ) ⇒
(let ((D+ (subsume A D+))) (lambda (S+)
(let ((D+ (subsume T D+))) (cond
(let ((D (append D+ D))) ((eq? S+ S ) #f)
(unit ‘(,S ,D ,A ,T ))))))))))) (else (cons (prefix-S S+ S ) D)))))
(define prefix-S (else D))))
(lambda (S+ S )
(define post-verify-D
(cond
(lambda (S D A T )
((eq? S+ S ) ’())
(cond
(else (cons (car S+) (prefix-S (cdr S+) S ))))))
((verify-A A S ) ⇒
(define subsume (post-verify-A S D T ))
(lambda (A/T D) (else #f))))
(remp (lambda (d ) (exists (subsumed-pr? A/T ) d ))
(define verify-A
D)))
(lambda (A S )
(define subsumed-pr? (cond
(lambda (A/T ) ((null? A) ’())
(lambda (pr-d ) ((verify-A (cdr A) S ) ⇒
(let ((u (rhs pr-d ))) (lambda (A0 )
(cond (let ((u (walk (lhs (car A)) S ))
((var? u) #f) (tag (pr
tag (car A)))
(else (pred (pr
pred (car A))))
(let ((pr (assq (lhs pr-d ) A/T ))) (cond
(and pr ((var? u)
(let ((tag (pr
tag pr ))) (cond
(cond ((ext-A u tag pred S A0 ) ⇒
((and (tag? tag) (lambda (A+)
(tag? u) (append A+ A0 )))
(tag=? u tag))) (else #f)))
(((pr
pred pr ) u) #f) (else (and (pred u) A0 ))))))
(else #t))))))))))) (else #f))))

17
(define post-verify-A (define update-D/T+
(lambda (S D T ) (lambda (x T+ S D T )
(lambda (A) (cond
(let ((D (subsume A D))) ((null? T )
(cond ‘(,D . ,T+))
((verify-T T S ) ⇒ (post-verify-T S D A)) (else
(else #f)))))) (let ((t (car T ))
(T (cdr T )))
(define verify-T (cond
(lambda (T S ) ((eq? (lhs t) x )
(cond (let ((D (ext-D x (pr
tag t) D S )))
((null? T ) ’()) (update-D/T+ x T+ S D T )))
((verify-T (cdr T ) S ) (else
⇒ (verify-T+ (lhs (car T )) T S )) (let ((T+ (cons t T+)))
(else #f)))) (update-D/T+ x T+ S D T )))))))))
(define verify-T+ (define ext-D
(lambda (x T S ) (lambda (x tag D S )
(lambda (T0 ) (cond
(let ((tag (pr
tag (car T ))) ((exists
(pred (pr
pred (car T )))) (lambda (d )
(case-value (walk x S ) (and (null? (cdr d ))
((x ) (cond (let ((y (lhs (car d )))
((ext-T+ x tag pred S T0 ) ⇒ (u (rhs (car d ))))
(lambda (T+) (append T+ T0 ))) (and
(else #f))) (eq? (walk y S ) x )
((au du) (cond (tag? u)
(((verify-T+ au T S ) T0 ) ⇒ (tag=? u tag)))))
(verify-T+ du T S )) D)
(else #f))) D)
((u) (and (pred u) T0 ))))))) (else (cons ‘((,x . ,tag)) D)))))
(define post-verify-T The final goal constructor, absent o , takes a tag, which
(lambda (S D A) must be a symbol, and a term u (possibly a variable), and
(lambda (T ) generates a constraint requiring that that tag not occur
(subsume-T T S (subsume T D) A ’())))) within the term.
The main driver of absent o is absento+, which takes care
(define subsume-T of the three possible types of terms: variables, pairs, and
(lambda (T+ S D A T ) ground values.
(let ((x∗ (rem-dups (map lhs A)))) If the term is a variable, we add the constraint provided it
(subsume-T+ x∗ T+ S D A T )))) is not already present. For ground values, we ensure that the
ground value does not in fact match the tag, which would
(define subsume-T+ violate the constraint. For pairs, we recur on the car and the
(lambda (x∗ T+ S D A T ) cdr , which might themselves generate further constraints.
(cond This guarantees that every pair has a left-hand side that is
((null? x∗ ) (let ((T (append T+ T ))) a variable and a right-hand side that contains both the tag
‘(,S ,D ,A ,T ))) and a predicate that determines whether other tags do not
(else (let ((x (car x∗ )) (x∗ (cdr x∗ ))) match (using the value returned by make-pred-T ).
(let ((D/T (update-D/T x S D A T+))) ext-T is the helper which actually adds the newly-formed
(let ((D (car D/T )) (T+ (cdr D/T ))) constraint to T , provided it is not already present.
(subsume-T+ x∗ T+ S D A T ))))))))
(define make-pred-T
(define update-D/T (lambda (tag)
(lambda (x S D A T ) (lambda (x )
(cond (not (and (tag? x ) (tag=? x tag))))))
((null? A) (let ((T (remp (lambda (t) (define absent o
(eq? (lhs t) x )) (lambda (tag u)
T ))) (cond
‘(,D . ,T ))) ((not (tag? tag)) fail )
(else (else
(let ((a (car A))) (λG (c : S D A T )
(cond (cond
((and (eq? (lhs a) x ) ((absento+ u tag c S D A T )
(or (tag=? (pr
tag a) ’sym) ⇒ unit)
(tag=? (pr
tag a) ’num))) (else (mzero))))))))
(update-D/T+ x ’() S D T ))
(else (update-D/T x S D (cdr A) T ))))))))

18
(define absento+ The function rem-dups generates a list of unique logic
(lambda (u tag c S D A T ) variables. It is used in two places, both times merely to avoid
(case-value (walk u S ) re-doing computations.
((x ) (define var (lambda (dummy) (vector dummy)))
(let ((T+ (ext-T x tag S T ))) (define var? (lambda (x ) (vector? x )))
(cond
((null? T+) c) (define rem-dups
(else (lambda (x∗ )
(let ((D (subsume T+ D))) (cond
(subsume-T T+ S D A T )))))) ((null? x∗ ) ’())
((au du) ((memq (car x∗ ) (cdr x∗ ))
(let ((c (absento+ au tag c S D A T ))) (rem-dups (cdr x∗ )))
(and c (else (cons (car x∗ )
(let ((S (c
S c)) (rem-dups (cdr x∗ )))))))
(D (c
D c))
(A (c
A c)) (define tag?
(T (c
T c))) (lambda (tag)
(absento+ du tag c S D A T ))))) (symbol? tag)))
((u)
(cond (define tag=?
((and (tag? u) (tag=? u tag)) #f) (lambda (tag1 tag2 )
(else c)))))) (eq? tag1 tag2 )))

(define ext-T (define lhs (lambda (pr ) (car pr )))

(lambda (x tag S T ) (define rhs (lambda (pr ) (cdr pr )))
(cond (define succeed (≡ #f #f))
((null? T ) (define fail (≡ #f #t))
(let ((pred (make-pred-T tag)))
‘((,x . (,tag . ,pred ))))) This definition of walk assumes a simple representation
(else of substitutions. Various persistent structures, such as those
(let ((t (car T )) (T (cdr T ))) in (Okasaki 1999), would improve the performance.
(let ((t-tag (pr
tag t))) (define walk
(cond (lambda (u S )
((eq? (walk (lhs t) S ) x ) (cond
(cond ((and (var? u) (assq u S )) ⇒
((tag=? t-tag tag) ’()) (lambda (pr ) (walk (rhs pr ) S )))
(else (ext-T x tag S T )))) (else u))))
((tag=? t-tag tag)
(let ((t-pred (pr
pred t))) D.3 The Unifier
(ext-T+ x tag t-pred S T )))
Below is unify, which uses triangular substitutions (Baader
(else (ext-T x tag S T )))))))))
and Snyder 2001) instead of the more common idempotent
(define ext-T+ substitutions. After possibly walking the first two arguments
(lambda (x tag pred S T ) to get a representative, the two-pairs case is treated. Oth-
(cond erwise, if there are not two pairs, then unify-nonpair gets
((null? T ) ‘((,x . (,tag . ,pred )))) the two representatives, which might extend the substitu-
(else tion. There is no explicit recursion in unify-nonpair , but
(let ((t (car T ))) unify-nonpair
√ calls ext-S , which calls a recursive function,
(let ((t-tag (pr
tag t))) occurs .
(cond (define unify
((eq? (walk (lhs t) S ) x ) (lambda (u v S )
(cond (let ((u (walk u S )) (v (walk v S )))
((tag=? t-tag tag) ’()) (cond
(else ((and (pair? u) (pair? v ))
(ext-T+ x tag pred S (let ((S (unify (car u) (car v ) S )))
(cdr T ))))) (and S (unify (cdr u) (cdr v ) S ))))
(else (else (unify-nonpair u v S ))))))
(ext-T+ x tag pred S
(cdr T )))))))))) (define unify-nonpair
(lambda (u v S )
D.2 miniKanren Helpers (cond
We have chosen vectors to represent logic variables merely ((eq? u v ) S )
as a simple way to distinguish variables from other valid ((var? u) (ext-S u v S ))
datatypes. This could have been avoided any number of ((var? v ) (ext-S v u S ))
ways. For example, each variable could have been given a ((equal? u v ) S )
unique index. (else #f))))

19
(define ext-S The remaining helpers form the final value, which in-
(lambda (x v S ) cludes relevant information in the constraints.
(case-value v (define reify
((y) (cons ‘(,x . ,y) S )) (lambda (x )
((au du) (cond √ (lambda (c)
((occurs x v S ) #f) (let ((S (c
S c)) (D (c
D c))
(else (cons ‘(,x . ,v ) S )))) (A (c
A c)) (T (c
T c)))
((v ) (cons ‘(,x . ,v ) S ))))) (let ((v (walk∗ x S )))
√ (let ((S (reify-S v ’())))
(define occurs
(reify+ v S
(lambda (x v S )
(let ((D (remp
(case-value (walk v S )
(lambda (d ) (anyvar? d S ))
((y) (eq? y x )) √ D)))
((av dv ) (or (occurs√ x av S ) (rem-subsumed D))
(occurs x dv S ))) (remp
((v ) #f)))) (lambda (a)
(var? (walk (lhs a) S )))
D.4 The Reifier
A)
The role of reify is to make the relevant information that (remp
is stored in the final state final-c (see run) as accessible (lambda (t)
as possible. Realizing that there might be a lot of relevant (var? (walk (lhs t) S )))
information about the variables in the final value of the T ))))))))
variable created in run makes it essential that much care In the definition of reify+ below, we have removed the
goes into writing the reifier. Specifically, we insist on a kind predicates from tag-predicate pairs of A and T , but we still
of Church-Rosser property (Barendregt 1984). Regardless use the names A and T to refer to these new data structures.
of how a program is written, if it terminates it should be
equal to every semantically equivalent program. For exam- (define reify+
ple, swapping conjuncts in a fresh should not change the (lambda (v S D A T )
appearance of the answers. But this equality must hold for (let ((D (subsume A D)))
D, A, and T which is why we sort lexicographically. (let ((A (map (lambda (a)
reify-S is the heart of the reifier. reify-S takes an arbi- (let ((x (lhs a))
trary value v and a substitution S , and returns a substi- (tag (pr
tag a)))
tution that maps every distinct variable in v to a unique ‘(,x . ,tag)))
symbol. The trick to maintaining left-to-right ordering of A))
the subscripts on these symbols is to process v from left to (T (map (lambda (t)
right, as can be seen in the case of reify-S which handles (let ((x (lhs t))
pairs. When reify-S encounters a variable, it determines if (tag (pr
tag t)))
we already have a mapping for that entity. If not, reify-S ‘(,x . ,tag)))
extends the substitution with an association between the T )))
variable and a new, appropriately-subscripted symbol built (form (walk∗ v S )
using reify-name. (walk∗ D S )
(walk∗ A S )
(define walk∗ (rem-subsumed-T (walk∗ T S )))))))
(lambda (v S )
(case-value (walk v S ) (define form
((x ) x ) (lambda (v D A T )
((av dv ) (let ((fd (drop-dot-D (sorter (map sorter D))))
(cons (walk∗ av S ) (walk∗ dv S ))) (f a (sorter (map sort-part (partition∗ A))))
((v ) v )))) (ft (drop-dot-T (sorter T ))))
(let ((fb (append ft f a )))
(define reify-S (cond
(lambda (v S ) ((and (null? fd ) (null? fb)) v )
(case-value (walk v S ) ((null? fd ) ‘(,v . ,fb))
((x ) (let ((n (length S ))) ((null? fb) ‘(,v . ((6≡ . ,fd ))))
(let ((name (reify-name n))) (else ‘(,v (6≡ . ,fd ) . ,fb)))))))
(cons ‘(,x . ,name) S ))))
((av dv ) (let ((S (reify-S av S ))) (define drop-dot-D
(reify-S dv S ))) (lambda (D)
((v ) S )))) (map (lambda (d )
(map (lambda (pr )
(define reify-name (let ((x (lhs pr ))
(lambda (n) (u (rhs pr )))
(string
symbol ‘(,x ,u)))
(string-append " " "." (number
string n))))) d ))
D)))

20
(define drop-dot-T (define unify∗
(lambda (T ) (lambda (S+ S )
(map (lambda (t) (unify (map lhs S+) (map rhs S+) S )))
(let ((x (lhs t))
(tag (rhs t))) (define part
‘(absent ,tag ,x ))) (lambda (tag A x∗ y∗ )
T ))) (cond
((null? A)
(define sorter (lambda (ls) (sort lex 6? ls))) (cons ‘(,tag . ,x∗ ) (partition∗ y∗ )))
((tag=? (rhs (car A)) tag)
(define sort-part (let ((x (lhs (car A))))
(lambda (pr ) (let ((x∗ (cond
(let ((tag (car pr )) ((memq x x∗ ) x∗ )
(x∗ (sorter (cdr pr )))) (else (cons x x∗ )))))
‘(,tag . ,x∗ )))) (part tag (cdr A) x∗ y∗ ))))
(define anyvar? (else
(lambda (u S ) (let ((y∗ (cons (car A) y∗ )))
(case-value u (part tag (cdr A) x∗ y∗ ))))))
((x ) (var? (walk x S ))) (define partition∗
((au du) (or (anyvar? au S ) (lambda (A)
(anyvar? du S ))) (cond
((u) #f)))) ((null? A) ’())
(define rem-subsumed (else
(lambda (D) (part (rhs (car A)) A ’() ’())))))
(let loop ((D D) (D+ ’())) The definition of lex 6? along with datum
string uses the
(cond effectful operator display, The functional version is tedious,
((null? D) D+) because of the number of different built-in Scheme types,
((or (subsumed? (car D) (cdr D)) and we have opted to use this version instead.
(subsumed? (car D) D+))
(define lex 6?
(loop (cdr D) D+))
(lambda (x y)
(else (loop (cdr D)
(string 6? (datum
string x ) (datum
string y))))
(cons (car D) D+)))))))
(define datum
string
(define subsumed?
(lambda (x )
(lambda (d D)
(call-with-string-output-port
(cond
(lambda (p) (display x p)))))
((null? D) #f)
(else (let ((dˆ (unify∗ (car D) d ))) D.5 Impure Control Operators
(or (and dˆ (eq? dˆ d )) For completeness, we define three additional miniKanren
(subsumed? d (cdr D)))))))) goal constructors: project, which can be used to access the
(define rem-subsumed-T values of variables, and conda and condu , which can be
(lambda (T ) used to prune the search tree of a program. The examples
(let loop ((T T ) (Tˆ ’())) from Thin Ice of The Reasoned Schemer (Friedman et al.
(cond 2005) demonstrate how conda and condu can be useful
((null? T ) Tˆ) and the pitfalls that await the unsuspecting reader. Also,
(else we have included an additional operator once o , defined in
(let ((x (lhs (car T ))) terms of condu , which forces the input goal to succeed at
(tag (rhs (car T )))) most once.
(cond (define-syntax project
((or (subsumed-T? x tag (cdr T )) (syntax-rules ()
(subsumed-T? x tag Tˆ)) (( (x . . . ) g g∗ . . . )
(loop (cdr T ) Tˆ)) (λG (c : S D A T )
(else (loop (cdr T ) (let ((x (walk∗ x S )) . . . )
(cons (car T ) Tˆ)))))))))) ((fresh () g g∗ . . . ) c))))))
(define subsumed-T? (define-syntax conda
(lambda (x tag1 T ) (syntax-rules ()
(cond (( (g0 g . . . ) (g1 ĝ . . . ) . . . )
((null? T ) #f) (λG (c)
(else (inc
(let ((y (lhs (car T ))) (if a ((g0 c) g . . . )
(tag2 (rhs (car T )))) ((g1 c) ĝ . . . ) . . . ))))))
(or
(and (eq? y x ) (tag=? tag2 tag1 ))
(subsumed-T? x tag1 (cdr T ))))))))

21
(define-syntax if a
(syntax-rules ()
(( ) (mzero))
(( (e g . . . ) b . . . )
(let loop ((c∞ e))
(case∞ c∞
(() (if a b . . . ))
((f ) (inc (loop (f ))))
((a) (bind∗ c∞ g . . . ))
((a f ) (bind∗ c∞ g . . . )))))))
(define-syntax condu
(syntax-rules ()
(( (g0 g . . . ) (g1 ĝ . . . ) . . . )
(λG (c)
(inc
(if u ((g0 c) g . . . )
((g1 c) ĝ . . . ) . . . ))))))
(define-syntax if u
(syntax-rules ()
(( ) (mzero))
(( (e g . . . ) b . . . )
(let loop ((c∞ e))
(case∞ c∞
(() (if u b . . . ))
((f ) (inc (loop (f ))))
((c) (bind∗ c∞ g . . . ))
((c f ) (bind∗ (unit c) g . . . )))))))
(define once o (lambda (g) (condu (g))))

22