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
(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)
(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))))
(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)))))
A value that has been walk*ed would mean that any resultant value which is a variable is fresh.
(walk* y ((y . (w z c)) (v . b) (x . v) (z . x))) ;; Gives us (w b c)