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