# 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)