MiniKanren core walk

(walk z ((z . a) (x . w) (y . z))) ;; Gives us a, we walk from var z to rhs of its association, a
(walk y ((z . a) (x . w) (y . z))) ;; Gives us a, we walk from y -> z -> a
(walk x ((x . y) (z . x) (y . z))) ;; Never stop walking due to cycle x -> y -> z -> x

With a substitution, s built by unify, (walk x s) will always have a value.

s won’t have walk-cycles as seen in the 3rd example above.

If walk has a value, the two possible types of values it can have is A) a fresh variable (since the variable is not associated, the walk terminates and returns the fresh var) B) a value that is not a variable (we can no longer walk since nothing is associated with primitives)

Definition

(define walk
  (lambda (v s) ;; Walk from a vertex, v through our substitution, s
    (cond
      ((var? v) ;; Is v a variable
        (cond
          ((assq v s) => ;; Implication; if we are able to bind v using the association list
            (lambda (a)
              (walk (rhs a) s))) ;; Continue to walk through
            (else v)))
      ;; If it isn't just return the variable itself
      (else v))))

walk*

(define walk*
  (lambda (v s)
    (let ((v (walk v s))) ;; Terminates at primitives / pairs / no binding
      (cond

        ((var? v) v) ;; If v is a variable, just return the variable and it must be fresh

        ((pair? v)   ;; If v is a pair
          (cons      ;; Walk each element
            (walk* (car v) s)   
            (walk* (cdr v) s)))

        (else v)))))

Invariant

A value that has been walk*ed would mean that any resultant value which is a variable is fresh.

Examples

(walk* y
  ((y . (w z c)) (v . b) (x . v) (z . x)))

;; Gives us (w b c)