staticKanren.tex

\section{STATICKANREN}\label{static}
This section introduces staticKanren, a language designed to analyze miniKanren programs. We first step through a few simple examples in Section \ref{static_intro} to develop intuition for the detailed implementation in Section \ref{static_imp}. Sections \ref{S} and \ref{au} demonstrate some applications of the language.

\subsection{Introductory examples}\label{static_intro}
On the surface, staticKanren was designed to look as close to miniKanren as possible. However, there are still some fundamental differences. Unlike miniKanren, staticKanren cannot deal with infinite answer streams. In fact, staticKanren programs can only return all answers using \code{run*}, as there is no point withholding already-computed answers. On one hand, this is unfortunate since we cannot write non-trivial recursive relations as-is. But on the other hand, this also gives the language a simpler implementation.

staticKanren offers only three primitive constraints: equality, disequality and \textbf{fake}. The first two retain their syntax and semantics from miniKanren, whereas the third is a new addition to emulate recursive relations. There is no reason not to include more primitive constraints. The more knowledge staticKanren has, the better answers it can return. However, adding other constraints would be a distraction from our goal, hence we only include disequality because it plays such an important role in many relations.

The core idea of staticKanren is the observation that relational programs' answers are themselves relational programs. And because answers are interpreted as programs, the language must treat variable names more seriously, as seen below:

\begin{lstlisting}
(run* (q p) (== q 4))
\end{lstlisting}
$\Rightarrow$ \code{(((4 #(p 0)) () ()))}

It should be noted that $\Rightarrow$ by default means "evaluating under staticKanren" in this section. If the above program were run under miniKanren instead, the answer would have been \code{((4 _.0))}. The variable \code{p} remains unknown in the answer, so it gets to keep its name. Remember that terms of the form \code{#(...)} are vectors, thus the variable bound to \code{p} is the vector \code{#(p 0)}\footnote{Variables in miniKanren have always been vectors, but we cannot not see that because variables are always reified to symbols at the end.} (let us ignore the number on the right for now). Besides the walked query, staticKanren always returns two additional constraint stores, one for disequalities and one for fake constraints. Therefore, every answer has the normal shape of a three-element list, which is good for computers and may not be intuitive for humans. The next example demonstrates how the language deals with name conflict:

\begin{lstlisting}
(run* (q a) (fresh (a d) (== q `(,a . ,d))))
\end{lstlisting}
$\Rightarrow$ \code{((((#(a 1) . #(d 1)) #(a 0)) () ()))}

The same program under miniKanren would return \code{(((_.0 . _.1) _.2))} instead. There are two variables having the same name \code{a}. staticKanren can still distinguish these two variables by their \textbf{birthdate} (the number shown on the right). Meanwhile, miniKanren sidesteps this problem completely by introducing a new name for every unbound variable appearing in the answer. It is perhaps a subjective matter to debate which representation is better, but there is at least one theoretical problem avoided by the new approach\footnote{This example was even mentioned in one of the online miniKanren's Uncourse Hangouts organized by William Byrd.}:

\begin{lstlisting}
(run* (q p) (== q '_.0))
\end{lstlisting}
$\Rightarrow$ \code{(((_.0 #(p 0)) () ()))}

The same program under miniKanren would return \code{((_.0 _.0))}!. And because two Scheme symbols are the same iff they look the same, there is no way to distinguish \code{p} and \code{q} in that case, even from the computer's perspective. The last example below demonstrates fake constraints:
\begin{lstlisting}
(run* (q p r)
  (fake `(mother ,q ,p)) (fake `(father ,p ,r))))
\end{lstlisting}

This is a meaningless program to stress that these fake constraints have no actual meaning. The \code{fake} form does no more than evaluating its body and adding the resulting expression to the fake constraint store.

$\Rightarrow$
\begin{lstlisting}
(((#(q 0) #(p 0) #(r 0))
 ()
 ((father #(p 0) #(r 0))
  (mother #(q 0) #(p 0)))))}
\end{lstlisting}



\subsection{Implementation}\label{static_imp}
This section presents an R6RS compliant implementation of staticKanren. The discussion will highlight only those parts containing interesting differences from the simple miniKanren implementation in \textcite{byrdphd}\footnote{The full implementation is available at \url{https://github.com/lackhoa/staticKanren}.}.

The following functions construct and dispatch variables. Variables are vectors of two elements: its name (a symbol) and its birthdate (a number). Additionally, we would like to have a total order on variables defined by \code{var>?}. A variable is greater than another if its birthdate is less (i.e. it was introduced sooner), or if it has the same birthdate and a lexicographically lesser name. Greater variables are called \textbf{seniors} and lesser ones are called \textbf{juniors}.
\begin{lstlisting}
(;; name is a symbol, bd is a number
 define var (lambda (name bd) (vector name bd)))
(define var->name (lambda (var) (vector-ref var 0)))
(define var->bd (lambda (var) (vector-ref var 1)))
(define var? vector?)
(define var>?
  ;; v1 is prioritized over v2
  (lambda (v1 v2)
    (let ([n1 (symbol->string (var->name v1))]
          [bd1 (var->bd v1)]
          [n2 (symbol->string (var->name v2))]
          [bd2 (var->bd v2)])
      (or (< bd1 bd2)
          (and (= bd1 bd2) (string<? n1 n2))))))
\end{lstlisting}

Next we have definitions concerning states. A state is a 4-tuple consisting of a substitution \code{S}, a date counter \code{C}, a disequality store \code{D} and a fake constraint store \code{F}. The counter starts from 0 and only goes upwards. \code{letg@} is a special form to extract constraints from states.
\begin{lstlisting}
(define-syntax letg@
  ;; let with state inspection
  (syntax-rules (:)
    [(_ (c : s* ...) e)
     (let ([s* (c-> c 's*)] ...) e)]))
(define all-constraints '(S C D F))
(define init-S '())
(define init-C 0)
(define init-D '())
(define init-F '())
(define make-c (lambda (S C D F) (list S C D F)))
(define init-c (make-c init-S init-C init-D init-F))
(define c->
  (lambda (c store)
    (rhs (assq store (map list all-constraints c)))))
(define update-S (lambda (c S) (letg@ (c : C D F) (make-c S C D F))))
(define update-C (lambda (c C) (letg@ (c : S D F) (make-c S C D F))))
(define update-D (lambda (c D) (letg@ (c : S C F) (make-c S C D F))))
(define update-F (lambda (c F) (letg@ (c : S C D) (make-c S C D F))))
\end{lstlisting}

The final piece of groundwork concerns the answer stream monad. Because there are no laziness, these definitions are trivial and we keep them here only for the sake of comparison.
\begin{lstlisting}
(define mzero (lambda () '()))
(define unit (lambda (x) `(,x)))
(define choice (lambda (x y) `(,x . ,y)))
(define mplus append)
(define bind (lambda (c* g) (apply mplus (map g c*))))
\end{lstlisting}

The first interesting function is \code{unify}, which takes two terms along with a substitution and returns the extended substitution where these two terms are made the same. In the case that they are always different, however, \code{unify} returns \code{#f}. There is a new clause in staticKanren to handle the case where both walked terms are variables, which makes sure that the senior is always on the rhs. That way, walked seniors never result in juniors.
\begin{lstlisting}
(define unify
  (lambda (t1 t2 S)
    (let ([t1 (walk t1 S)]
          [t2 (walk t2 S)])
      (cond
       [(eq? t1 t2) S]
       [(and (var? t1) (var? t2))
        (cond
         [(var>? t2 t1) (extend t1 t2 S)]
         [else (extend t2 t1 S)])]
       [(var? t1) (extend-check t1 t2 S)]
       [(var? t2) (extend-check t2 t1 S)]
       [(and (pair? t1) (pair? t2))
        (let ([S+ (unify (car t1) (car t2) S)])
          (and S+ (unify (cdr t1) (cdr t2) S+)))]
       [(equal? t1 t2) S]
       [else #f]))))
\end{lstlisting}

The new clause (to compare variables) adds a little runtime overhead, but that does not matter in this case because this function simply is not used at runtime. There is a method to achieve the same effect without modifying \code{unify} by tweaking the reification process instead, which should eliminate the runtime overhead. However, doing it in this way keeps the substitution list clean and easy to work with. This cleanliness is helpful in section \ref{au} where we have to modify the substitution list after reification.

Figures \ref{miniS} and \ref{staticS} show both miniKanren's and staticKanren's representations of the same variable-only substitution. Each vertex corresponds to a variable and each edge from vertex \code{x} to vertex \code{y} corresponds to an association with lhs \code{x} and rhs \code{y}.

\begin{figure}[h]
    \centering
    \begin{minipage}{.5\textwidth}
        \includegraphics[height=.5\textwidth]{figures/miniS.png}
        \captionof{figure}{miniKanren's substitution}
        \label{miniS}
    \end{minipage}%
    \begin{minipage}{.5\textwidth}
        \includegraphics[height=.5\textwidth]{figures/staticS.png}
        \captionof{figure}{staticKanren's substitution}
        \label{staticS}
    \end{minipage}
\end{figure}

Now we are ready to define user-level functions, starting with the fake goal constructor. It should be remembered that \code{lambdag@} is a \code{lambda} form with the ability to extract various constraints from its argument, which is always a state.
\begin{lstlisting}
(define fake
  (lambda (expr)
    (lambdag@ (c : F)
      (unit (update-F c `(,expr . ,F))))))
\end{lstlisting}

The job of \code{fresh} is broken down to a conjunction (\code{conj}) which strings goals together and a \code{letv} which creates variables. \code{letv} extracts the date counter from its input state and assigns it to the new variables. The counter is then incremented before getting fed to the goal in its body.
\begin{lstlisting}
(define-syntax fresh
  (syntax-rules ()
    [(_ (x* ...) g g* ...)
     (letv (x* ...) (conj g g* ...))]))

(define-syntax letv
  (syntax-rules ()
    [(_ (x* ...) g)
     (lambdag@ (c : C)
       (let ([x* (var 'x* C)] ...)
         (g (update-C c (+ C 1)))))]))
\end{lstlisting}

Other goal constructors do not need to be modified. Surprisingly, reification can be made simpler despite the fact that unknown variables get to keep their names. To obtain the answers, \code{reify} only needs to deep walk the query and the constraint stores in \code{c}. A more compact representation of disequality is then obtained by removing constraints containing either no variable or irrelevant variables (i.e. variables absent from both deep walked \code{q*} and deep walked \code{F}).
\begin{lstlisting}
(define reify
  ;; This will return a c with clausal S
  (lambda (c q*)
    (letg@ (c : S D F)
      (let ([t (walk* q* S)]
            [D (walk* D S)]
            [F (walk* F S)])
        (let ([R (get-vars `(,t ,F))])
          (let ([D (rem-subsumed (purify-D D R))])
            `(,t ,D ,F)))))))
\end{lstlisting}

Some helpers of \code{reify} are given below. It is worth noting that miniKanren data are also miniKanren terms, which explains why the code can be so short. The function performing subsumption check of disequality stores, \code{rem-subsumed}, remains unchanged.
\begin{lstlisting}
(define-syntax case-term
  ;; A type dispatcher for mk terms
  (syntax-rules ()
    [(_ e [v e1] [(a d) e2] [atom e3])
     (let ([term e])
       (cond
        [(var? term) (let ([v term]) e1)]
        [(pair? term)
          (let ([a (car term)] [d (cdr term)]) e2)]
        [else (let ([atom term]) e3)]))]))

(define purify-D
  (lambda (D R)
    (filter (lambda (d)
              (not (or (constant? d)
                       (has-iv? d R))))
            D)))

(define has-iv?
  (lambda (t R)
    (let has-iv? ([t t])
      (case-term t
        [v (not (memq v R))]
        [(a d) (or (has-iv? a) (has-iv? d))]
        [atom #f]))))
\end{lstlisting}

Finally, the definition of \code{run*} is as follows:
\begin{lstlisting}
(define-syntax run*
  (syntax-rules ()
    [(_ (q q* ...) g g* ...)
     ((fresh (q q* ...)
        g g* ...
        (finalize `(,q ,q* ...)))
      init-c)]))

(define finalize
  (lambda (qs)
    (lambdag@ (final-c)
      (unit (reify final-c qs)))))
\end{lstlisting}
This concludes the core implementation of staticKanren.

\subsection{Returning substitutions in answers}\label{S}
Let us begin exploring the practical value of staticKanren with a simple improvement: returning substitutions instead of walked queries in the answers. We achieve this with the new \code{run*su} form. For instance, the answers in the next call would be \code{((#(p 0) #(p 0) #(p 0)) () ())} if we replaced \code{run*su} by \code{run*}.
\begin{lstlisting}
(run*su (q p r) (== q p) (== p r))
\end{lstlisting}
$\Rightarrow$ \code{((((#(r 0) #(p 0)) (#(q 0) #(p 0))) () ()))}

We see that the answer looks exactly like the program, which once again highlights the fact that miniKanren states are just accumulations of logical assertions throughout the execution of programs, albeit normalized. By looking at the answers, we can summarize the content of the program that produced them. As a matter of fact, answers may be simpler than programs, as the following case shows:
\begin{lstlisting}
(pp (run*su (q p) (== q p) (== p q)))
\end{lstlisting}
$\Rightarrow$ \code{((((#(q 0) #(p 0))) () ()))}

Since \code{==} is commutative, the assertion \code{(== p q)} is redundant and it is removed from the final answer. It might look as if a complex inference mechanism is involved, but in fact this feature only requires a simple addition to \code{run*}. We can retrieve a substitution simply by unifying the query with the walked version of itself, which is what would be returned by \code{run*}. The definition \code{run*su} is given below:
\begin{lstlisting}
(define-syntax run*su
  ;; run* with substitutions
  (syntax-rules ()
    [(_ (q q* ...) g g* ...)
     (let ([q (var 'q init-C)] [q* (var 'q* init-C)] ...)
       (let ([qs `(,q ,q* ...)])
         (let ([c* ((conj g g* ... (finalize qs))
                    (update-C init-c (+ init-C 1)))])
           (map (lambda (c) (su c qs)) c*))))]))

(define su
  (lambda (c qs)
    (let ([t (car c)])
      `(,(unify t qs init-S)
        .
        ,(cdr c)))))
\end{lstlisting}

This much of development already lets us to obtain the "negative" side of the \code{lookupt} function defined earlier in Section \ref{reif}. Before running it in staticKanren, however, we need to first redefine \code{lookupt}, so that the recursive call is fake as follows.
\begin{lstlisting}
(define lookupt
  (lambda (x env t)
    (lambda (bound?)
      (conde
       [Unchanged ...]
       [(fresh (y b rest)
          (== `((,y . ,b) . ,rest) env)
          (condo
           [Unchanged ...]
           [else
            (;; The only place that is changed
             fake `((lookupt ,x ,rest ,t) ,bound?))]))]))))
\end{lstlisting}

\begin{lstlisting}
(run*su (x env) ((lookupt x env 'unbound) #f))
\end{lstlisting}
$\Rightarrow$
\begin{lstlisting}
(((#(x 0) ())
  () 
  ())
 ((#(x 0) 
   ((#(y 1) . #(b 1)) . #(rest 1)))
  (((#(y 1) #(x 0))))
  (((lookupt #(x 0) #(rest 1) unbound) #f))))
\end{lstlisting}
This response is akin to the goal:
\begin{lstlisting}
(conde
 [(== '() x)]
 [(== `((,y . ,b) . ,rest) x)
  (=/= y x)
  ((lookupt x rest 'unbound) #f)])
\end{lstlisting}
The second clause is particularly interesting: it states that if the environment is non-empty and the lookup is to fail, the variable \code{x} must not match the association's lhs and the lookup must also fail for the rest of the environment.

\subsection{Obtaining common unification with anti-unification}\label{au}
There are still cases where rewritten programs do not look at all similar to the original. Take \code{membero} for example:
\begin{lstlisting}
(define membero
  ;; (run* (x) (membero x '(a b c)))
  ;; (without fake goal) => (a b c)
  (lambda (x ees)
    (fresh (e es)
      (== ees `(,e . ,es))
      (condo
       [(==t x e) succeed]
       [else (fake `(membero ,x ,es))]))))
\end{lstlisting}

Rewriting through \code{run*su} gives us the following:
\begin{lstlisting}
((((#(ees 0) (#(x 0) . #(es 1)))) 
  ()
  ())
 (((#(ees 0) (#(e 1) . #(es 1))))
  (((#(e 1) #(x 0))))
  ((membero #(x 0) #(es 1)))))
\end{lstlisting}
The answer above is equivalent to this program:
\begin{lstlisting}
(define membero
  (lambda (x ees)
    (conde
     [(fresh (es)
        (== `(,x . ,es) ees))]
     [(fresh (e es)
        (== `(,e . ,es) ees)
        (=/= e x)
        (membero x es))])))
\end{lstlisting}
Human readers would agree that the version above does not look at all natural: it does not show the common structure of \code{ees} in both clauses. To make this notion of commonness clear, we introduce \textbf{anti-unification}, a dual of unification. Given a collection of terms, anti-unification returns their least general generalization. This process describes quite well humans' ability to recognize patterns over symbolic formulae, which is exactly what we need for this purpose. The following is an example of anti-unification:
\begin{lstlisting}
(let ([t* '((1 * 2 = 2 + 1)
            (4 * 3 = 3 + 4))])
  (anti-unify t*))
\end{lstlisting}
$\Rightarrow$ \code{(#(au0 0.5) * #(au1 0.5) = #(au1 0.5) + #(au0 0.5))}

Anti-unification has captured the common pattern from these two formulae. \code{au0} and \code{au1} are normal staticKanren variables introduced in the process, which from now on shall be referred to as \textbf{pattern variables}. All pattern variables have the birthdate \code{0.5}, the reason for which will become clear when the program is complete.

The implementation of \code{anti-unify} is adapted from \textcite{ostvold2004functional}. The most significant difference is that this version also recognizes identical variables as being the same terms and reuses that variable in the pattern. \code{anti-unify} is given below:

\begin{lstlisting}
(define anti-unify
  (lambda (t*)
    (let-values
        ([(res _iS)
          (let au ([t* t*] [iS '()])
            (cond
             [;; rule 7: eq? deals with variables too
              (for-all (eqp? (car t*)) (cdr t*))
              (values (car t*) iS)]
             [;; rule 8
              (for-all pair? t*)
              (let-values ([(a iS+) (au (map car t*) iS)])
                (let-values ([(d iS++)
                              (au (map cdr t*) iS+)])
                  (values `(,a . ,d) iS++)))]
             [;; rule 9
              (find (lambda (s) (teq? (lhs s) t*)) iS)
              =>
              (lambda (s) (values (rhs s) iS))]
             [;; rule 10
              else
              (let ([new-var
                     (var (au-name (length iS)) AU-BD)])
                (values new-var (extend t* new-var iS)))]))])
      res)))

(define eqp? (lambda (u) (lambda (v) (eq? u v))))

(define teq?
  ;; Compares two mk terms
  (lambda (t1 t2)
    (or (eq? t1 t2)
        (and (pair? t1) (pair? t2)
             (teq? (car t1) (car t2))
             (teq? (cdr t1) (cdr t2))))))

(define au-name
  (lambda (n)
    (string->symbol
     (string-append "au" (number->string n)))))
\end{lstlisting}

Even though anti-unification is the heart of our solution, there is still a lot of work to do. It is not clear how to convert the obtained pattern into a usable program. We start with a similar definition to Section \ref{S}:
\begin{lstlisting}
(define-syntax run*au
  ;; run* with anti-unification analysis
  (syntax-rules ()
    [(_ (q q* ...) g g* ...)
     (let ([q (var 'q init-C)] [q* (var 'q* init-C)] ...)
       (let ([qs `(,q ,q* ...)])
         (let ([c* ((conj g g* ... (finalize qs))
                    (update-C init-c (+ init-C 1)))])
           (au-extract c* qs))))]))
\end{lstlisting}

The main work is now delegated to \code{au-extract}, which takes the answers and the query as input. First, \code{au-extract} extracts a common pattern \code{au} from the walked query \code{t*}. Second, it unifies the query with the pattern in the empty environment, resulting in the substitution \code{uS}. The next obvious step is to unify \code{au} back into each of the walked queries in \code{t*} to obtain the substitutions \code{S*}. Finally, we perform the optional step of cleaning up the substitutions with \code{purify-S} and deep walk the other constraints, obtaining a working program. This is shown below:
\begin{lstlisting}
(define au-extract
  (lambda (c* qs)
    (let ([t* (map car c*)]
          [D* (map cadr c*)]
          [F* (map caddr c*)])
      (let ([au (anti-unify t*)])
        (let ([auS (unify qs au init-S)])
          (let ([S* (map (lambda (t)
                           (prefix-unify au t auS))
                         t*)])
            `(,(purify-S auS init-C)
              ,(map au-helper S* D* F*))))))))

(define prefix-unify
  (lambda (t1 t2 S) (prefix-S (unify t1 t2 S) S)))

(define au-helper
  (lambda (S D F)
    (let ([S (purify-S S AU-BD)]
          [D (walk* D S)]
          [F (walk* F S)])
      `(,S ,D ,F))))

(define AU-BD (+ init-C 0.5))
\end{lstlisting}

The only question left is how to clean up the substitutions. We have already done a similar thing during reification with the help of \code{walk*}. However, this time things are not so convenient since we also want to retain the intermediate associations given by anti-unification. There is a basic principle that works well: an association is redundant iff its lhs (a variable) was not introduced prior to a certain date. The intuitive reason is that we can just use the rhs in the first place without ever introducing the lhs.

Conveniently, \code{purify-S} can keep track of already introduced variables using their birthdates. Associations whose lhs was born later than a certain date (called the \textbf{cutoff date}) are filtered out of the substitution list. We need only look at the lhs because it is always the junior variable in the case that both sides are variables. The definition of \code{purify-S} is as follows:
\begin{lstlisting}
(define purify-S
  (lambda (S cutoff)
    (filter (lambda (s) (<= (var->bd (lhs s)) cutoff))
            S)))
\end{lstlisting}

Looking back, we see that \code{purify-S} is called twice in \code{au-extract} and \code{au-helper}. The first call is to clean up the common substitution involving query variables and pattern variables, in which case the cutoff date only allows query variables (note that \code{init-C} is also the birthdate of all query variables). In the second call (in \code{au-helper}) which involves case-specific substitutions, we also include pattern variables since they have already been introduced. This explains why pattern variables are born on \code{0.5}: they are junior to query variables, but senior to all variables introduced by the "user" (i.e. variables coming from \code{fresh}). Figure \ref{fig:au_S} illustrates the idea.
\begin{figure}[h]
    \centering
    \includegraphics{figures/au_S.png}
    \caption{The interaction between query, pattern and "user" variables}
    \label{fig:au_S}
\end{figure}


The implementation is now complete and we can start using \code{run*au} to rewrite programs. The call below will return \code{lookupo}, obtained by forcing \code{lookupt} to "return" \code{#t}. Notice that this \code{lookupt} is the same modified version in section \ref{S}.
\begin{lstlisting}
(run*au (x env t) ((lookupt x env t) #t))
\end{lstlisting}
$\Rightarrow$
\begin{lstlisting}
(((#(env 0)
   ((#(au0 0.5) #(au1 0.5)) . #(rest 1))))
 ((((#(au1 0.5) #(t 0))
    (#(au0 0.5) #(x 0)))
   ()
   ())
  (()
   (((#(au0 0.5) #(x 0))))
   (((lookupt #(x 0) #(rest 1) #(t 0))
     #t)))))
\end{lstlisting}
This response is akin to the goal:
\begin{lstlisting}
(fresh (au0 au1)
  (== `((,au0 . ,au1) . ,rest) env)
  (conde
   [(== au0 x) (== t au1)]
   [(=/= au0 x)
    ((lookupt x rest t) #t)]))
\end{lstlisting}
Anti-unification identifies that across all clauses, the environment \code{env} is always a non-empty list with the first element being an association. It also correctly handles what each clause has to do afterwards to obtain the original semantics. Especially the third clause is a clever assertion: it says that if the association's lhs (\code{au0}) is different from the variable \code{x} and the lookup is to succeed, the lookup of \code{x} in the tail of the environment has to succeed.

To aid in understanding what the role of \code{purify-S} is in the example above, here is the same answer but with both calls to \code{purify-S} removed:
\begin{lstlisting}
(((#(env 0)
   ((#(au0 0.5) #(au1 0.5)) . #(rest 1))))
 ((((#(au1 0.5) #(t 0))
    (#(au0 0.5) #(x 0)))
   ()
   ())
  (((#(b 1) #(au1 0.5))
    (#(y 1) #(au0 0.5)))
   (((#(au0 0.5) #(x 0))))
   (((lookupt #(x 0) #(rest 1) #(t 0))
     #t)))))
\end{lstlisting}
This is akin to the goal:
\begin{lstlisting}
(fresh (au0 au1)
  (== `((,au0 ,au1) . ,rest) env)
  (conde
   [(== au0 x) (== au1 t)]
   [(== b au1) (== y au0)
    (=/= au0 x)
    ((lookupt x rest t) #t)]))
\end{lstlisting}
The two \code{==}'s involving \code{b} and \code{y} are not necessary and were removed by the second call to \code{purify-S} in the original answer due to the fact that \code{b} and \code{y} were born after \code{AU-BD} (0.5).