Relational Programming

Introduction
What is relational programming?
μKanren
Dissecting μKanren
μKanren in practice
Sweetening μKanren with a bit of syntax sugar
Related books

Introduction

I'm at the very beginning of learning about logic, relational programming, miniKanren, Prolog, etc. This page contains my personal notes as well as links to papers and talks I found interesting. At the end of the page there is a list of related books for those that want to dig deeper.

If you want to subscribe to this page, use this RSS feed.

What is relational programming?

According to Wikipedia in relation to logic programming:

The term relational programming has been used to cover a variety of programming languages that treat functions as a special case of relations.

William E. Byrd provides a great introduction to relational programming during his talk "A New Relational Language" at the Houston FPUG (Functional Programming Users Group). I tried to summarize it bellow these lines.

In functional programming, given the following expression in Lisp syntax:

(+ 3 4) => 7

We say that + is a function that takes the numbers 3 and 4 and returns their sum, which is 7.

In other words, there is the notion of:

Function (+)
Inputs (3 and 4)
Output (7)

Meanwhile, in relational programming, this is expressed in terms of relations. Our previous example becomes the following relation:

(+o 3 4 7)

Which is a 4-place relation where functional programming's dichotomy between inputs and outputs is gone. Note that +o in relational programming is equivalent to + in functional programming.

Relations are very flexible because, in addition to the notion of a relation, we are going to think of in terms of algebra and algebraic reasoning. So, we can replace any position in a relation with a variable. Then, we can query the system for possible values of those variables.

For instance,

(+o 3 4 Z) => Z = 7

or,

(+o 3 Y 7) => Y = 4

or,

(+o X Y 7) => X = 0; Y = 7
              X = 1; Y = 6
	      ...

In short, relational programming removes the idea of input vs output.

μKanren

μKanren is a minimalist language in the miniKanren family of relational programming languages.

The miniKanren family of languages is detailed in the thesis "Relational Programming in miniKanren: Techniques, Applications, and Implementations" by William E. Byrd.

What follows is the μKanren implementation exposed on the paper "μKanren: A Minimal Functional Core for Relational Programming" by Jason Hemann and Daniel P. Friedman. The code has been commented with the relevant parts of the paper and is available here.

 1: ;; Variables are represented as vectors that hold their variable
 2: ;; index.  Variable equality is determined by coincidence of indices
 3: ;; in vectors.
 4: (define (var c) (vector c))
 5: (define (var? x) (vector? x))
 6: (define (var=? x1 x2) (= (vector-ref x1 0) (vector-ref x2 0)))
 7: 
 8: ;; The walk operator searches for a variable's value in the
 9: ;; substitution.  When a non-variable term is walked, the term itself
10: ;; is returned.
11: (define (walk u s)
12:   (let ((pr (and (var? u) (assp (lambda (v) (var=? u v)) s))))
13:     (if pr (walk (cdr pr) s) u)))
14: 
15: ;; The ext-s operator extends the substitution with a new binding.
16: ;; When extending the substitution, the first argument is always a
17: ;; variable and the second is an arbitrary term.
18: (define (ext-s x v s) `((,x . ,v) . ,s))
19: 
20: ;; The ≡ goal constructor takes two terms as arguments and returns a
21: ;; goal that succeeds if those two terms unify in the received state.
22: ;; If those two terms fail to unify in that state, the empty stream is
23: ;; instead returned.
24: (define (≡ u v)
25:   (lambda (s/c)
26:     (let ((s (unify u v (car s/c))))
27:       (if s (unit `(,s . ,(cdr s/c))) mzero))))
28: 
29: ;; unit lifts the state into a stream whose only element is that
30: ;; state.
31: (define (unit s/c) (cons s/c mzero))
32: 
33: ;; mzero is the empty stream.
34: (define mzero '())
35: 
36: ;; Terms of the language are defined by the unify operator.  Here,
37: ;; terms of the language consist of variables, objects deemed
38: ;; identical under eqv?, and pairs of the foregoing.  To unify two
39: ;; terms in a substitution, both are walked in that substitution.  If
40: ;; the two terms walk to the same variable, the original substitution
41: ;; is returned unchanged.  When one of the two terms walks to a
42: ;; variable, the substitution is extended, binding the variable to
43: ;; which that term walks with the value of which the other term walks.
44: ;; If both terms walk to pairs, the cars and then cdrs are unifed
45: ;; recursively, succeeding if unification succeeds in the one and then
46: ;; the other.  Finally, non-variable, non-pair terms unify if they are
47: ;; identical under eqv?, and unification fails otherwise.
48: (define (unify u v s)
49:   (let ((u (walk u s)) (v (walk v s)))
50:     (cond
51:      ((and (var? u) (var? v) (var=? u v)) s)
52:      ((var? u) (ext-s u v s))
53:      ((var? v) (ext-s v u s))
54:      ((and (pair? u) (pair? v))
55:       (let ((s (unify (car u) (car v) s)))
56:         (and s (unify (cdr u) (cdr v) s))))
57:      (else (and (eqv? u v) s)))))
58: 
59: ;; The call/fresh goal constructor takes a unary function f whose body
60: ;; is a goal, and itself returns a goal.  This returned goal, when
61: ;; provided a state s/c, binds the formal parameter of f to a new
62: ;; logic variable, and passes a state, with the substitution it
63: ;; originally received and a newly incremented fresh-variable counter,
64: ;; c, to the goal that is the body of f.
65: (define (call/fresh f)
66:   (lambda (s/c)
67:     (let ((c (cdr s/c)))
68:       ((f (var c)) `(,(car s/c) . ,(+ c 1))))))
69: 
70: ;; The disj goal constructor takes two goals as arguments and returns
71: ;; a goal that succeeds if either of the two subgoals succeed.
72: (define (disj g1 g2) (lambda (s/c) (mplus (g1 s/c) (g2 s/c))))
73: 
74: ;; The conj goal constructor similarly takes two goals as arguments
75: ;; and returns a goal that succeeds if both goals succeed for that
76: ;; state.
77: (define (conj g1 g2) (lambda (s/c) (bind (g1 s/c) g2)))
78: 
79: ;; The search strategy of μKanren is encoded through the mplus and
80: ;; bind operators.
81: 
82: ;; The mplus operator is responsible for merging streams.
83: (define (mplus $1 $2)
84:   (cond
85:    ((null? $1) $2)
86:    ((procedure? $1) (lambda () (mplus $2 ($1))))
87:    (else (cons (car $1) (mplus (cdr $1) $2)))))
88: 
89: ;; bind invokes the goal g on each element of the stream $.  If the
90: ;; stream is empty or becomes exhausted mzero, the empty stream, is
91: ;; returned.
92: (define (bind $ g)
93:   (cond
94:    ((null? $) mzero)
95:    ((procedure? $) (lambda () (bind ($) g)))
96:    (else (mplus (g (car $)) (bind (cdr $) g)))))

μKanren was also shown in the talk "Implementing a microKanren" that Jason Hemann and Daniel P. Friedman gave at Code Mesh 2016.

Dissecting μKanren

This μKanren implementation weights 39 lines of code. Being so short makes easier to experiment with it. However, it also hides lots of details. In this section I try to analyze every single bit of it to get a better understanding.

Variables

Variables are represented as vectors:

1: (include "relational-programming/ukanren.ss")
2: (var 0)

#(0)

The 0-th index of the vector is the variable index.

1: (include "relational-programming/ukanren.ss")
2: (define x (var 0))
3: (vector-ref x 0)

Two variables are equal if their indices are equal.

1: (include "relational-programming/ukanren.ss")
2: (define x (var 0))
3: (define y (var 0))
4: (define z (var 1))
5: (printf "x == y => ~a == ~a => ~a\n" x y (var=? x y))
6: (printf "x == z => ~a == ~a => ~a\n" x z (var=? x z))

x == y => #(0) == #(0) => #t
x == z => #(0) == #(1) => #f

Substitutions

A substitution is an association list that binds variables to concrete values or to other variables. A substitution can be extended using the ext-s operator.

1: (include "relational-programming/ukanren.ss")
2: (define s '())
3: (define s (ext-s (var 0) 'arbitrary-term s))
4: (define s (ext-s (var 1) (var 0) s))
5: s

((#(1) . #(0)) (#(0) . arbitrary-term))

The walk operator searches for a variable's value in the substitution recursively.

1: (include "relational-programming/ukanren.ss")
2: (define s '((#(1) . #(0)) (#(0) . arbitrary-term)))
3: (walk (var 1) s)

arbitrary-term

When a variable is not bound, the variable itself is returned.

1: (include "relational-programming/ukanren.ss")
2: (define s '((#(1) . #(0))))
3: (walk (var 1) s)

#(0)

Goals

A goal is represented as a function that takes a state and returns a stream. A state is a pair of a substitution and a non-negative integer representing a fresh variable counter. A stream is a sequence of states.

μKanren provides the following goal constructors: ≡, disj and conj.

The ≡ goal constructor takes two terms as arguments and returns a goal that succeeds if those two terms unify in the received state. If those two terms fail to unify in that state, the empty stream is instead returned.

1: (include "relational-programming/ukanren.ss")
2: (define s/c '(() . 0))
3: (define g (≡ (var 0) 5))
4: (g s/c)

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

Note that the goal does not increment the fresh variable counter. That is why the call/fresh goal constructor exists.

The call/fresh goal constructor takes a unary function f whose body is a goal, and itself returns a goal. This returned goal, when provided a state s/c, binds the formal parameter of f to a new logic variable, and passes a state, with the substitution it originally received and a newly incremented fresh-variable counter to the goal that is the body of f.

1: (include "relational-programming/ukanren.ss")
2: (define s/c '(() . 0))
3: (define f (lambda (q) (≡ q 5)))
4: ((call/fresh f) s/c)

((((#(0) . 5)) . 1))

If the two terms of ≡ fail to unify, the empty stream should be returned.

1: (include "relational-programming/ukanren.ss")
2: (define s/c '(() . 0))
3: (define f (lambda (q) (≡ 3 5)))
4: ((call/fresh f) s/c)

()

The unification of 3 and 5 fails because these terms are not identical. We can also verify that the unification of 5 and 5—or q and q in general—succeeds but do not extend the stream.

1: (include "relational-programming/ukanren.ss")
2: (define s/c '(() . 0))
3: (define f (lambda (q) (≡ 5 5)))
4: ((call/fresh f) s/c)

((() . 1))

1: (include "relational-programming/ukanren.ss")
2: (define s/c '(() . 0))
3: (define f (lambda (q) (≡ q q)))
4: ((call/fresh f) s/c)

((() . 1))

The disj goal constructor takes two goals as arguments and returns a goal that succeeds if either of the two subgoals succeed.

1: (include "relational-programming/ukanren.ss")
2: (define s/c '(() . 0))
3: ((disj
4:   (call/fresh (lambda (q) (≡ q 3)))
5:   (call/fresh (lambda (q) (≡ q 5)))) s/c)

((((#(0) . 3)) . 1) (((#(0) . 5)) . 1))

The conj goal constructor similarly takes two goals as arguments and returns a goal that succeeds if both goals succeed for that state.

1: (include "relational-programming/ukanren.ss")
2: (define s/c '(() . 0))
3: ((conj
4:   (call/fresh (lambda (q) (≡ q 3)))
5:   (call/fresh (lambda (q) (≡ q 5)))) s/c)

((((#(1) . 5) (#(0) . 3)) . 2))

Unification

Unification is determined by the unify operator of the μKanren implementation. It is especially interesting that it is unify that defines the terms of the language. In this implementation terms of the language consist of variables, objects deemed identical under eqv? and pairs of the foregoing.

To unify two terms in a substitution, both are walked in that substitution. If the two terms walk to the same variable, the original substitution is returned unchanged.

1: (include "relational-programming/ukanren.ss")
2: (define s '((#(0) . 5) (#(1) . #(0)) (#(2) . #(0))))
3: (unify (var 1) (var 2) s)

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

When one of the two terms walks to a variable, the substitution is extended, binding the variable to which that term walks with the value of which the other term walks.

1: (include "relational-programming/ukanren.ss")
2: (define s '((#(0) . 5) (#(2) . #(0))))
3: (unify (var 1) (var 2) s)

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

1: (include "relational-programming/ukanren.ss")
2: (define s '((#(0) . 5) (#(2) . #(1))))
3: (unify (var 2) 3 s)

((#(1) . 3) (#(0) . 5) (#(2) . #(1)))

1: (include "relational-programming/ukanren.ss")
2: (define s '((#(0) . 5) (#(2) . #(0))))
3: (unify (var 1) 3 s)

((#(1) . 3) (#(0) . 5) (#(2) . #(0)))

If both terms walk to pairs, the cars and then cdrs are unifed recursively, succeeding if unification succeeds in the one and then the other.

1: (include "relational-programming/ukanren.ss")
2: (define s '())
3: (unify `(,(var 0) . ,(var 1)) '(3 . 5) s)

((#(1) . 5) (#(0) . 3))

Finally, non-variable, non-pair terms unify if they are identical under eqv?.

1: (include "relational-programming/ukanren.ss")
2: (define s '((#(0) . 5)))
3: (unify (var 0) 5 s)

((#(0) . 5))

1: (include "relational-programming/ukanren.ss")
2: (define s '())
3: (unify 5 5 s)

()

Unification fails otherwise.

1: (include "relational-programming/ukanren.ss")
2: (define s '((#(0) . 5)))
3: (unify (var 0) 3 s)

#f

1: (include "relational-programming/ukanren.ss")
2: (define s '())
3: (unify 5 3 s)

#f

The `mplus` and `bind` operators

The mplus operator is responsible for merging streams.

1: (include "relational-programming/ukanren.ss")
2: (define $1 '((((#(0) . 3)) . 1) (((#(0) . 5)) . 1)))
3: (define $2 '((((#(0) . 7)) . 1)))
4: (mplus $1 $2)

((((#(0) . 3)) . 1) (((#(0) . 5)) . 1) (((#(0) . 7)) . 1))

The disj constructor is defined in terms of the mplus operator. It takes two goals— g1 and g2 —and returns the stream that results from merging (g1 s/c) and (g2 s/c).

(define (disj g1 g2) (lambda (s/c) (mplus (g1 s/c) (g2 s/c))))

The bind operator invokes a goal on each element on a stream.

1: (include "relational-programming/ukanren.ss")
2: (define $ '((((#(0) . 3)) . 1) (((#(0) . 5)) . 1)))
3: (define g (call/fresh (lambda (q) (≡ q 7))))
4: (bind $ g)

((((#(1) . 7) (#(0) . 3)) . 2) (((#(1) . 7) (#(0) . 5)) . 2))

The conj constructor is defined in terms of the bind operator. It takes two goals— g1 and g2 —and returns the stream that results from invoking g2 on each element of the stream returned by (g1 s/c).

(define (conj g1 g2) (lambda (s/c) (bind (g1 s/c) g2)))

Both mplus and bind are able to return a stream without computing the answers it contains. These are called inmature streams and allow to represent infinite streams.

 1: (include "relational-programming/ukanren.ss")
 2: (define empty-state '(() . 0))
 3: (define (fives x)
 4:   (disj (≡ x 5) (lambda (s/c) (lambda () ((fives x) s/c)))))
 5: (define (sixes x)
 6:   (disj (≡ x 6) (lambda (s/c) (lambda () ((sixes x) s/c)))))
 7: (define fives-and-sixes
 8:   (call/fresh (lambda (x) (disj (fives x) (sixes x)))))
 9: (define stream (fives-and-sixes empty-state))
10: 
11: (printf "~a\n" stream)
12: (printf "~a\n" ((cdr stream)))
13: (printf "~a\n" ((cdr ((cdr stream)))))
14: (printf "~a\n" ((cdr ((cdr ((cdr stream)))))))

((((#(0) . 5)) . 1) . #<procedure at ukanren.ss:3504>)
((((#(0) . 6)) . 1) . #<procedure at ukanren.ss:3504>)
((((#(0) . 5)) . 1) . #<procedure at ukanren.ss:3504>)
((((#(0) . 6)) . 1) . #<procedure at ukanren.ss:3504>)

μKanren in practice

The following is a very simple example of how to use the core functionality of μKanren:

1: (include "relational-programming/ukanren.ss")
2: (define empty-state '(() . 0))
3: (define a-and-b
4:   (conj
5:    (call/fresh (lambda (a) (≡ a 7)))
6:    (call/fresh (lambda (b) (disj (≡ b 5) (≡ b 6))))))
7: (a-and-b empty-state)

((((#(1) . 5) (#(0) . 7)) . 2) (((#(1) . 6) (#(0) . 7)) . 2))

Now let's implement appendo, which is considered the "Hello, world" of the relational programming languages.

 1: (include "relational-programming/ukanren.ss")
 2: (define empty-state '(() . 0))
 3: 
 4: (define (appendo l s o)
 5:   (disj
 6:    (conj (≡ l '()) (≡ s o))
 7:    (call/fresh
 8:     (lambda (a)
 9:       (call/fresh
10:        (lambda (d)
11:          (conj
12:           (≡ l `(,a . ,d))
13:           (call/fresh
14:            (lambda (r)
15:              (conj
16:               (≡ `(,a . ,r) o)
17:               (lambda (s/c) (lambda () ((appendo d s r) s/c)))))))))))))
18: 
19: (define stream (call/fresh
20:                 (lambda (x)
21:                   (call/fresh
22:                    (lambda (y)
23:                      (appendo x y '(a b c)))))))
24: 
25: (printf "~a\n" (stream empty-state))
26: (printf "~a\n" ((cdr (stream empty-state))))
27: (printf "~a\n" ((cdr ((cdr (stream empty-state))))))
28: (printf "~a\n" ((cdr ((cdr ((cdr (stream empty-state))))))))

((((#(1) a b c) (#(0))) . 2) . #<procedure at ukanren.ss:3504>)
((((#(1) b c) (#(3)) (#(4) b c) (#(2) . a) (#(0) #(2) . #(3))) . 5) . #<procedure at ukanren.ss:3504>)
((((#(1) c) (#(6)) (#(7) c) (#(5) . b) (#(3) #(5) . #(6)) (#(4) b c) (#(2) . a) (#(0) #(2) . #(3))) . 8) . #<procedure at ukanren.ss:3504>)
((((#(1)) (#(9)) (#(10)) (#(8) . c) (#(6) #(8) . #(9)) (#(7) c) (#(5) . b) (#(3) #(5) . #(6)) (#(4) b c) (#(2) . a) (#(0) #(2) . #(3))) . 11))

A closer look at the results shows that the values found for x and y are:

x = ()       y = (a b c)
x = (a)      y = (b c)
x = (a b)    y = (c)
x = (a b c)  y = ()

Note that if we remove the boilerplate, it is quite easy to see the correspondence between the append and appendo implementations:

(define (appendo l s o)
  (disj (conj (≡ l '()) (≡ s o))
        (conj (≡ l `(,a . ,d))
              (conj (≡ `(,a . ,r) o)
                    (appendo d s r) s/c))))

(define (append l s)
  (cond ((null? l) s)
        (else (cons (car l)
                    (append (cdr l) s)))))

Sweetening μKanren with a bit of syntax sugar

μKanren off-loads higher level operations, like the ones provided by miniKanren, to the user (e.g. run, run*, fresh, etc.). The μKanren paper presents a reference implementation for some helpers. The following code includes those helpers as well as a custom reifier that makes easier to read the returned results. The code is available here.

  1: ;; Zzz allows to write a delayed goal like
  2: ;;   (lambda (s/c)
  3: ;;     (lambda ()
  4: ;;       (g s/c)))
  5: ;; as
  6: ;;   (Zzz g)
  7: (define-syntax Zzz
  8:   (syntax-rules ()
  9:     ((_ g) (lambda (s/c) (lambda () (g s/c))))))
 10: 
 11: ;; conj+ allows to write nested calls to conj like
 12: ;;   (conj g0
 13: ;;         (conj g1
 14: ;;               g2))
 15: ;; as
 16: ;;   (conj+ g0 g1 g2)
 17: (define-syntax conj+
 18:   (syntax-rules ()
 19:     ((_ g) (Zzz g))
 20:     ((_ g0 g ...) (conj (Zzz g0) (conj+ g ...)))))
 21: 
 22: ;; disj+ allows to write nested calls to disj like
 23: ;;   (disj g0
 24: ;;         (disj g1
 25: ;;               g2))
 26: ;; as
 27: ;;   (disj+ g0 g1 g2)
 28: (define-syntax disj+
 29:   (syntax-rules ()
 30:     ((_ g) (Zzz g))
 31:     ((_ g0 g ...) (disj (Zzz g0) (disj+ g ...)))))
 32: 
 33: ;; conde allows to write the common pattern
 34: ;;   (disj+ (conj+ g0 g1 g2)
 35: ;;          (conj+ g3 g4 g5)
 36: ;;          (conj+ g6 g7 g8))
 37: ;; as
 38: ;;   (conde
 39: ;;     (g0 g1 g2)
 40: ;;     (g3 g4 g5)
 41: ;;     (g6 g7 g8))
 42: (define-syntax conde
 43:   (syntax-rules ()
 44:     ((_ (g0 g ...) ...) (disj+ (conj+ g0 g ...) ...))))
 45: 
 46: ;; fresh allows to write nested calls to call/fresh like
 47: ;;   (call/fresh
 48: ;;     (lambda (x)
 49: ;;       (call/fresh
 50: ;;         (lambda (y)
 51: ;;            (g x y)))))
 52: ;; as
 53: ;;   (fresh (x y) (g x y))
 54: (define-syntax fresh
 55:   (syntax-rules ()
 56:     ((_ () g ...) (conj+ g ...))
 57:     ((_ (x0 x ...) g ...) (call/fresh (lambda (x0) (fresh (x ...) g ...))))))
 58: 
 59: ;; pull automatically invokes an immature stream to return results.
 60: (define (pull $)
 61:   (if (procedure? $) (pull ($)) $))
 62: 
 63: ;; take-all pulls all the results from the stream.
 64: (define (take-all $)
 65:   (let (($ (pull $)))
 66:     (if (null? $) '() (cons (car $) (take-all (cdr $))))))
 67: 
 68: ;; take pulls n results from the stream.
 69: (define (take n $)
 70:   (if (zero? n)
 71:       '()
 72:       (let (($ (pull $)))
 73:         (if (null? $) '() (cons (car $) (take (- n 1) (cdr $)))))))
 74: 
 75: ;; empty-state represents the empty state.
 76: (define empty-state '(() . 0))
 77: 
 78: ;; call/empty-state attempts a goal in the empty state.
 79: (define (call/empty-state g) (g empty-state))
 80: 
 81: ;; run executes the provided goals and calls take, reifying the
 82: ;; results afterwards.
 83: (define-syntax run
 84:   (syntax-rules ()
 85:     ((_ n (x ...) g0 g ...)
 86:      (multivar-reify (x ...) (take n (call/empty-state
 87:                                       (fresh (x ...) g0 g ...)))))))
 88: 
 89: ;; run* executes the provided goals and calls take-all, reifying the
 90: ;; results afterwards.
 91: (define-syntax run*
 92:   (syntax-rules ()
 93:     ((_ (x ...) g0 g ...)
 94:      (multivar-reify (x ...) (take-all (call/empty-state
 95:                                         (fresh (x ...) g0 g ...)))))))
 96: 
 97: ;; multivar-reify reifies a list of states s/c* by refiying each
 98: ;; state's substitution with respect to each provided variable.
 99: (define-syntax multivar-reify
100:   (syntax-rules ()
101:     ((_ (x ...) s/c*)
102:      (map (lambda (s/c)
103:             (reify
104:              (let loop ((vs '(x ...)) (n 0))
105:                (if (null? vs)
106:                    '()
107:                    (cons (cons (car vs) (var n))
108:                          (loop (cdr vs) (+ n  1)))))
109:              s/c))
110:           s/c*))))
111: 
112: ;; The reify function takes a state s/c and an arbitrary value v,
113: ;; perhaps containing variables, and returns the reified value of v.
114: (define (reify v s/c)
115:   (let ((v (walk* v (car s/c))))
116:     (walk* v (reify-s v '()))))
117: 
118: ;; reify-s takes a walk*ed term as its first argument; its second
119: ;; argument starts out as an empty substitution.  The result of
120: ;; invoking reify-s is a reified name substitution, associating logic
121: ;; variables to distinct symbols of the form _.n.
122: (define (reify-s v s)
123:   (let ((v (walk v s)))
124:     (cond
125:      ((var? v) (ext-s v (reify-name (length s)) s))
126:      ((pair? v) (reify-s (cdr v) (reify-s (car v) s)))
127:      (else s))))
128: 
129: ;; reify-name generates a symbol of the form _.n.
130: (define (reify-name n)
131:   (string->symbol
132:    (string-append "_" "." (number->string n))))
133: 
134: ;; walk* deeply walks a term with respect to a substitution.
135: (define (walk* v s)
136:   (let ((v (walk v s)))
137:     (cond
138:      ((var? v) v)
139:      ((pair? v) (cons (walk* (car v) s)
140:                       (walk* (cdr v) s)))
141:      (else v))))

Let's apply them to our appendo example to make it more readable.

 1: (include "relational-programming/ukanren.ss")
 2: (include "relational-programming/ukanren-usr.ss")
 3: 
 4: (define (appendo l s o)
 5:   (fresh (a d r)
 6:          (conde ((≡ l '()) (≡ s o))
 7:                 ((≡ l `(,a . ,d))
 8:                  (≡ `(,a . ,r) o)
 9:                  (appendo d s r)))))
10: 
11: (run* (x y) (appendo x y '(a b c)))

(((x) (y a b c)) ((x a) (y b c)) ((x a b) (y c)) ((x a b c) (y)))

Related books

"Introduction to Logic" by Patrick Suppes
"The Little Lisper" by Daniel P. Friedman
"The Little Schemer, Fourth Edition" by Daniel P. Friedman and Matthias Felleisen
"The Reasoned Schemer, Second Edition" by Daniel P. Friedman, William E. Byrd, Oleg Kiselyov and Jason Hemann