On this page:
2.1 Variables
2.2 Substitutions
2.3 Unification
2.4 Reification
2.5 The run Interface
2.6 Examples
8.4

2 Implementing Unification

Put informal grammar here and push formal grammar to appendix

== is the fundamental operator on top using which other goals are built in miniKanren. Thus, the first goal that we will implement is ==.

2.1 Variables

== is a two argument operator that tries to unify its arguments. The arguments to unify may either be constants such as 7 or symbols such as foo, or variables. Furthermore, the arguments can also be arbitrary cons pairs of variables or constants or a combination of both. Therefore, we need a representation for variables that can be distinguished from all constants. To this end, we choose singleton vectors that wrap around an id number to represent variables by assuming that vectors cannot be used in the language being implemented itself. Thus, a variable is a number wrapped in a vector. We collectively refer to arguments that can be passed to == as terms.

(define (var c) (vector c))
(define var? vector?)
(define (var=? x1 x2) (= (vector-ref x1 0) (vector-ref x2 0)))

2.2 Substitutions

To implement unification, we first need to understand the concept of a substitution. Mathematically, a substitution is a mapping from a set of variables to a set of values. Our representation of substitutions will be a list of pairs, with the invariant that the car of any pair in a substitution be a variable. Thus, to extend a substitution we simply extend the underlying list (assuming the arguments passed do not break the invariant).

(define (ext-s u v s) `((,u . ,v) . ,s))

Now that we have a representation for substitutions, we also need a way to search for the value of a variable in a substitution. We do this using walk, which recursively keeps looking up the value of a term until it hits either a constant, or a variable with no further bindings in the substitution (we refer to such a variable as a "fresh" variable).

(define (walk u s)
  (let ([pr (and (var? u) (assp (lambda (v) (var=? u v)) s))])
    (if pr
      (walk (cdr pr) s)
      u)))

Here, assp returns the first pair whose car satisfies the passed predicate or false if there is no such pair.

(define (assp f x*)
  (match x*
    ['() #f]
    [`(,a . ,d)
     (if (f (car a))
       a
       (assp f d))]))

2.3 Unification

Now we define unify, which tries to unify two terms in a given substitution.

(define (unify u v s)
  (let ([u (walk u s)]
        [v (walk v s)])
    (cond
      [(and (var? u) (var? v) (var=? u v)) s]
      [(var? u) (ext-s u v s)]
      [(var? v) (ext-s v u s)]
      [(and (pair? u) (pair? v))
       (let ([s (unify (car u) (car v) s)])
         (and s (unify (cdr u) (cdr v) s)))]
      [else (and (eqv? u v) s)])))

We first walk both the terms in the substitution, then do a case-wise analysis. If both are variables that are already equal, then we simply return the substitution unchanged. The next two cases apply when both are variables that are not equal or only one of them is a variable. In the fourth case, we attempt to recursively unify cons pairs. The final case is to handle both terms being constants.

The state in this chapter will only have a single component — a substitution. However, as it will grow with the operators supported by our implementation, we wrap it in a list and define an accessor:

(define (s-of st)
  (car st))

With all the machinery needed at hand, we now define the == operator:
(define (== u v)
  (lambda (st)
    (let ([s (unify u v (s-of st))])
      (if s `(,s) '()))))

2.4 Reification

The final piece of implementation we need to make our miniKanren usable is the reifier, which translates the result of our interpreter into a human readable format.

(define (mk-reify st)
  (let ([v (walk* (var 0) (s-of st))])
    (walk* v (reify-s v '()))))

Since we only support a single variable, to reify this we walk* it in the substitution. walk* works just like walk, with the exception that recurs on pairs.

(define (reify-s v s)
  (let ([v (walk v s)])
    (cond
      [(var? v)
       (let ([n (reify-name (length s))])
         (cons `(,v . ,n) s))]
      [(pair? v) (reify-s (cdr v) (reify-s (car v) s))]
      [else s])))
 
(define (reify-name n)
  (string->symbol
    (string-append "_." (number->string n))))
 
(define (walk* v s)
  (let ([v (walk v s)])
    (cond
      [(var? v) v]
      [(pair? v) (cons (walk* (car v) s)
                       (walk* (cdr v) s))]
      [else v])))

2.5 The run Interface

We now utilize some syntactic sugar to get the usual run form:
(define empty-state '(()))
(define (call/empty-state g) (g empty-state))
 
(define-syntax run*
  (syntax-rules ()
    [(_ (x) g)
     (mk-reify
       (let ([x (var 0)])
         (call/empty-state g)))]))

2.6 Examples

Here are a few example programs that use all the features supported by our implementation so far:

> (run* (x) (== `(3 ,x) `(3 4)))
4
> (run* (x) (== '(3 4) x))
'(3 4)
> (run* (x) (== x x))
'.0
> (run* (x) (== 5 5))
'.0