On this page:
3.1 State
3.2 Updating Goals
3.3 Syntactic Sugar
3.4 Reification
3.5 The run Interface
3.6 Examples
8.4

3 Implementing fresh

So far we have restricted our programs to have only one logic variable. However, with a little effort we can add support for multiple variables. We will now extend our implementation to support multiple variables

3.1 State

When we had only one variable, we could get away by having just the substitution as our state. But when we want multiple variables, this is not sufficient to track all the variables introduced in our programs. Therefore, we extend the state to hold information about introduced variables via a counter. Now our state will be a pair where the car is a substitution and the cdr is a counter that counts the number of variables introduced so far. Thus, we can use the cdr of a state to create a new logic variable when needed. For example, the following is the state of a program with two variables where the zeroth variable is unified with 5:

(((#(0) . 5)) . 2)

3.2 Updating Goals

We first update our == goal to work with our new state:

(define (== u v)
  (lambda (s/c)
    (let ([s (unify u v (car s/c))])
      (if s `(,s . ,(cdr s/c)) '()))))

Next, we add call/fresh which lets us introduce new logic variables:

(define (call/fresh f)
  (lambda (s/c)
    (let ([c (cdr s/c)])
      ((f (var c)) `(,(car s/c) . ,(+ c 1))))))

Here f is expected to be a wrapper procedure around a goal. f is a single argument procedure whose only argument will be bound to the appropriate logic variable at the call site. Thus, the goal wrapped by f will use the lexical variable introduced by f as a logic vaiable. Since the state tells us what the next logic variable’s number will be, we create a logic variable with this number and apply f to it to unwrap the goal in f. We then pass the state to the goal with the counter incremented as we created a new logic variable.

3.3 Syntactic Sugar

To get the familiar miniKanren fresh, we utilize the following syntactic sugar:

(define-syntax fresh
  (syntax-rules ()
    [(_ () g) g]
    [(_ (x0 x ...) g)
     (call/fresh (lambda (x0) (fresh (x ...) g)))]))

3.4 Reification

We update our reifier to work with the new state:

(define (mk-reify s/c)
  (let ([v (walk* (var 0) (car s/c))])
    (walk* v (reify-s v '()))))

3.5 The run Interface

We update our empty state to fit our new state and the run interface to use fresh:
(define empty-state '(() . 0))
(define (call/empty-state g) (g empty-state))
 
(define-syntax run*
  (syntax-rules ()
    [(_ (x) g)
     (mk-reify
       (call/empty-state (fresh (x) g)))]))

3.6 Examples

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

(run* (x) (fresh (y) (== x y)))
(run* (x) (fresh (y z) (== (cons y z) x)))