reif.tex

\section{RELATIONAL CONDITIONALS WITH PSEUDO-FUNCTIONS}\label{reif}
\subsection{The problem with conde}
Suppose we need to write a relation called to retrieve a variable's value in an environment, call it \code{lookupo}. The task at first is just a straightforward transformation from the Scheme function \code{lookup} in the following way:
\begin{lstlisting}
(define lookup
  ;; (lookup 'x '([x 1] [y 2] [z 3]))
  ;; => 1
  (lambda (x env)
    (let ([a (car env)])
      (cond
       [(eq? x (lhs a)) (rhs a)]
       [else (lookup x (cdr env))]))))

(define lookupo
  ;; (run* (x t) (lookupo x '([x 1] [y 2] [z 3]) t))
  ;; => ((x 1) (y 2) (z 3))
  (lambda (x env t)
    (fresh (y b rest)
      (== `([,y ,b] . ,rest) env)
      (conde
       [(== y x) (== b t)]
       [(=/= y x) (lookupo x rest t)]))))
\end{lstlisting}

Later on we might need to actually handle the case where the variable is unbound instead of raising an error or fail. We update both definitions as follows:
\begin{lstlisting}
(define lookup
  ;; (lookup 'x '([x 1] [y 2]))
  ;; => (x 1)
  ;; (lookup 'z '([x 1] [y 2]))
  ;; => #f
  (lambda (x env)
    (cond
     [(null? env) #f]
     [else
      (let ([a (car env)])
        (cond
         [(eq? x (lhs a)) a]
         [else (lookup x (cdr env))]))])))

(define lookupo
  ;; (run* (x t bound) (lookupo x '([x 1] [y 2]) t bound?))
  ;; => ((x 1 #t)
  ;;     (y 2 #t)
  ;;     ((_.0 _.1 #f) (=/= ((_.0 x)) ((_.0 y)))))
  (lambda (x env t bound?)
    (conde
     [(== '() env) (== #f bound?)]
     [(fresh (y b rest)
        (== `((,y ,b) . ,rest) env)
        (conde
         [(== y x) (== #t bound?) (== b t)]
         [(=/= y x) (lookupo x rest t bound?)]))])))
\end{lstlisting}

So far so good: \code{lookup} only needs an additional relation argument indicating whether the variable is bound\footnote{We could also write another relation that succeeds precisely when lookup fails, but that approach would quickly lead to a dead end, as will be seen later.}. Meanwhile, we have to devise a special signal for \code{lookup}, namely \code{#f}, to indicate the unbound case\footnote{There is technically a way to return multiple values in Scheme but it is not too common, particularly due to the verbosity of the syntax.}. However, a problem arises when we actually use the output in \code{cond}. \code{case1} and \code{case1o} demonstrate essentially the same usage of \code{lookup(o)} (the main point is that these cases are analogous; it does not matter what they actually mean):
\begin{lstlisting}
(define case1
  (lambda (x env)
    (cond
     [(lookup x env) => rhs]
     [else #f])))

(define case1o
  (lambda (x env out)
    (conde
     [(lookupo x env out #t)]
     [(lookupo x env 'unbound #f)
      (== #f out)])))
\end{lstlisting}

Why can we not use \code{else} in the second clause? The reason is that despite the similarity in appearance, \code{conde} does not process its clauses from top to bottom like \code{cond} does, hence there can be no default case. As a result, programmers must always be prepared to append extra denials in lower \code{conde} clauses. This issue gets serious when the control flow is more complex, such as in \code{case2(o)} below:

\begin{lstlisting}
(define case2
  (lambda (x y env)
    (cond
     [(lookup x env) => rhs]
     [(lookup y env) => rhs]
     [else #f])))

(define case2o
  (lambda (x y env out)
    (conde
     [(lookupo x env out #t)]
     [(lookupo x env '? #f) (lookupo y env out #t)]
     [(lookupo x env '? #f) (lookupo y env '? #f)
      (== #f out)])))
\end{lstlisting}

This time there are three extra denials instead of just the one of \code{case1o}. The example above is still generous, as it is usual for relations to include four or more \code{conde} clauses. The number of extra denials exhibits quadratic growth, introducing opportunities for errors without any significant contribution to the meaning of the program. The next section shows a simple way to deal with this using a technique first implemented in Prolog by \textcite{reif}.

\subsection{Pseudo-function and condo}
miniKanren code looks primitive because all goals are actions manipulating implicit \textit{states}. For more complex combinations to work, there must be another way for relations to "communicate". \textbf{Pseudo-functions} achieve this communication by signaling their computed results. However, pseudo-functions receive their results as arguments instead of returning them. To make sense of this concept, the following transformation should be observed (the "t" at the end of names denote pseudo-functions, because it is too late to change):
\begin{lstlisting}
;; From function
(define bar (lambda (in) 'v))
;; To relation
(define baro (lambda (in out) (== out 'v)))
;; To pseudo-function...
(define bart (lambda (in) (lambda (out) (baro in out))))
;; ...which is equivalent to
(define bart (lambda (in) (lambda (out) (== out 'v))))
\end{lstlisting}

From a low-level point of view, a pseudo-function is a function which takes a single argument and returns a goal. The act of \textit{returning} a result is then mimicked by the goal's act of \textit{unifying} that single argument with the result. As an aside, a relation can be made to return whichever of its formal parameters, depending on the circumstance. Examples of this can be seen below:
\begin{lstlisting}
;; From relation
(define conso
  ;; (run* (a d ls) (conso x y))
  ;; => ((_.0 _.1 (_.0 . _.1)))
  (lambda (a d ls)
    (== `(,a . ,d) ls)))
;; To pseudo-function 1
(define cart
  ;; (run* (ls a) ((cart ls) a))
  ;; => (((_.0 . _.1) _.0))
  (lambda (ls)
    (lambda (a)
      (fresh (d) (conso a d ls)))))
;; To pseudo-function 2
(define cdrt
  ;; (run* (ls d) ((cdrt ls) d))
  ;; => (((_.0 . _.1) _.1))
  (lambda (ls)
    (lambda (d) (fresh (a) (conso a d ls)))))
;; To pseudo-function 3
(define const
  ;; (run* (a d ls) ((const a d) ls))
  ;; => ((_.0 _.1 (_.0 . _.1)))
  (lambda (a d)
    (lambda (ls)
      (conso a d ls))))
\end{lstlisting}
I have never encountered a situation where this is actually useful as there is generally only one parameter deemed "the output". It is worth noting that even though pseudo-functions act like pure functions, they can affect more than just the output. For instance, the goal \code{((cart x) a)} will always instantiate \code{x} to a pair, if it is currently unknown.

Getting back to the problem of conditionals, we first define below two trivial pseudo-functions \code{truet} and \code{falset} whose results are \code{#t} and \code{#f} respectively.

\begin{lstlisting}
(define truet
  ;; (run* (?) ((truet) ?))
  ;; => (#t)
  (lambda ()
    (lambda (?)
      (== #t ?))))

(define falset
  ;; (run* (?) ((falset) ?))
  ;; => (#f)
  (lambda ()
    (lambda (?)
      (== #f ?))))
\end{lstlisting}

Next, we define a single "primitive" pseudo-function similar to Scheme's \code{eq?}\footnote{Depending on the implementation, more primitives may be defined using additional primitive constraints.}. This function relies on both \code{==} and \code{=/=} to express two branches of the output.
\begin{lstlisting}
(define ==t
  ;; (run* (x y ?) ((==t x y) ?))
  ;; => ((_.0 _.0 #t)
  ;;     ((_.0 _.1 #f) (=/= ((_.0 _.1)))))
  (lambda (x y)
    (lambda (?)
      (conde
       [(== #t ?) (== x y)]
       [(== #f ?) (=/= x y)]))))
\end{lstlisting}

Next, we provide ways of creating more complex pseudo-functions from simpler ones, starting with \code{negt} (negation) below:
\begin{lstlisting}
(define negt
  (lambda (g)
    (lambda (?)
      (conde
       [(== #t ?) (g #f)]
       [(== #f ?) (g #t)]))))
\end{lstlisting}

From this, \code{=/=t} can be trivially derived as follows:
\begin{lstlisting}
(define =/=t
  ;; (run* (x y ?) ((=/=t x y) ?))
  ;; (((_.0 _.1 #t) (=/= ((_.0 _.1))))
  ;;  (_.0 _.0 #f))
  (lambda (x y)
    (negt (==t x y))))
\end{lstlisting}

Next, we define \code{conjt} (conjunction) and \code{disjt} (disjunction) using macro in the following ways:
\begin{lstlisting}
(define-syntax conjt
  (syntax-rules ()
    [(_) (truet)]
    [(_ g) g]
    [(_ g1 g2 gs ...)
     (lambda (?)
       (conde
        [(g1 #t) ((conjt g2 gs ...) ?)]
        [(== #f ?) (g1 #f)]))]))

(define-syntax disjt
  (syntax-rules ()
    [(_) (falset)]
    [(_ g) g]
    [(_ g1 g2 gs ...)
     (lambda (?)
       (conde
        [(== #t ?) (g1 #t)]
        [(g1 #f)  ((disjt g2 gs ...) ?)]))]))
\end{lstlisting}

The two following examples demonstrate conjunction and disjunction:
\begin{lstlisting}
(run* (t x y z)
   ((conjt (==t x y)
           (==t y z))
    t))
\end{lstlisting}
$\Rightarrow$
\begin{lstlisting}
(((#f _.0 _.1 _.2) (=/= ((_.0 _.1))))
 (#t _.0 _.0 _.0)
 ((#f _.0 _.0 _.1) (=/= ((_.0 _.1)))))
\end{lstlisting}

\begin{lstlisting}
(run* (t x y z)
   ((disjt (==t x y)
           (==t y z))
    t))
\end{lstlisting}
$\Rightarrow$
\begin{lstlisting}
((#t _.0 _.0 _.1)
 ((#t _.0 _.1 _.1) (=/= ((_.0 _.1))))
 ((#f _.0 _.1 _.2) (=/= ((_.0 _.1)) ((_.1 _.2)))))
\end{lstlisting}

Finally, we can define the goal constructor \code{condo} -- the closest relational counterpart of \code{cond}. We should keep in mind that \code{succeed} stands for the "do nothing" goal and \code{fail} stands for the "always fail" goal.
\begin{lstlisting}
(define-syntax condo
  (syntax-rules (else)
    [(_ [else]) succeed]
    [(_ [else g]) g]
    [(_ [else g1 g2 g* ...])
     (fresh () g1 g2 g* ...)]
    [(_ [test g* ...] c* ...)
     (conde
      [(test #t) g* ...]
      [(test #f) (condo c* ...)])]
    [(_) fail]))
\end{lstlisting}
\code{condo} is an interesting combinator, because it uses two types of objects: pseudo-functions in the test positions and normal miniKanren goals in the bodies of each clause. The \code{else} keyword can be used to signify the default case, although it can be omitted, in which case the program fails when no clause matches. The example below demonstrates the use of \code{condo}:
\begin{lstlisting}
(run* (x y z)
  (condo
   [(==t x y) succeed]
   [(==t y z) succeed]
   [else (== x z)]))
\end{lstlisting}
$\Rightarrow$
\begin{lstlisting}
((_.0 _.0 _.1)
 ((_.0 _.1 _.1) (=/= ((_.0 _.1))))
 ((_.0 _.1 _.0) (=/= ((_.0 _.1)))))
\end{lstlisting}

We are now able to replace \code{lookupo} with the pseudo-function \code{lookupt}, as seen below.
\begin{lstlisting}
(define lookupt
  ;; (run* (x t bound?) ((lookupt x '([x 1]) t) bound?))
  ;; => ((x 1 #t)
  ;;     ((_.0 _.1 #f) (=/= ((_.0 x)))))
  (lambda (x env t)
    (lambda (bound?)
      (conde
       [(== '() env)
        (== #f bound?)]
       [(fresh (y b rest)
          (== `((,y ,b) . ,rest) env)
          (condo
           [(==t y x) (== #t bound?) (== b t)]
           [else
            ((lookupt x rest t) bound?)]))]))))
\end{lstlisting}
Now, the following comparison between \code{case2} and \code{case2o} does not look so bad anymore:
\begin{lstlisting}
(define case2
  (lambda (x y env)
    (cond
     [(lookup x env) => rhs]
     [(lookup y env) => rhs]
     [else #f])))

(define case2o
  (lambda (x y env)
    (lambda (out)
      (condo
       [(lookupt x env out) succeed]
       [(lookupt y env out) succeed]
       [else (== #f out)]))))
\end{lstlisting}

Before converting all of your relations to pseudo-functions, there are still some issues to discuss. \code{condo} works it magic by hiding the control flow. And despite the enhanced readability that this technique brings, there is no simple way to see what is actually going on behind the layer of abstraction. As a result, it is easy to accidentally change the behavior of programs. Take for example the following goal using \code{condo}:
\begin{lstlisting}
(fresh (x y)
  (condo
   [(==t 'a x) (== 1 y)]
   [(==t 'b x) (== 2 y)]
   [(==t 'c x) (== 3 y)]))
\end{lstlisting}
It is not clear that there is an issue with this code, because it looks so much like normal Scheme. The issue only shows itself when we expand the \code{condo} as follows:
\begin{lstlisting}
(fresh (x y)
  (conde
   [(== 'a x) (== 1 y)]
   [(=/= 'a x) (== 'b x) (== 2 y)]
   [(=/= 'a x) (=/= 'b x) (== 'c x) (== 3 y)]))
\end{lstlisting}
Clearly, the additional denials in these \code{conde} clauses are redundant since they are already mutually exclusive. Moreover, switching from \code{conde} to \code{condo} always means changing the way miniKanren's search work, which might be devastating to some existing programs. As a result, we are once again stuck with lengthy, buggy \code{conde} clauses whose meaning cannot be easily grasped. The next section addresses this issue by offering a way to verify the correctness of existing programs with \textbf{staticKanren}.