How does append-to-form work? (SICP's section on Logic Programming)

I am currently working through SICP's section on Logic Programming, but I got stuck in the examples regarding logical deductions, especially the append-to-form rules. How do they work? What I don't quite understand is how the second rule cdr-downs the first list. For example, given:

(rule (append-to-form () ?y ?y))

(rule (append-to-form (?u . ?v) ?y (?u开发者_如何学C . ?z)) (append-to-form ?v ?y ?z))

a) How do we reach from:

;;; Query input:
(append-to-form (a b) (c d) ?z)

to

;;; Query results:
(append-to-form (a b) (c d) (a b c d))

b) And what bout this one:

;;; Query input:
(append-to-form (a b) ?y (a b c d))

to

;;; Query results:
(append-to-form (a b) (c d) (a b c d))

c) And lastly:

;;; Query input:
(append-to-form ?x ?y (a b c d))

to

;;; Query results:
(append-to-form () (a b c d) (a b c d))
(append-to-form (a) (b c d) (a b c d))
(append-to-form (a b) (c d) (a b c d))
(append-to-form (a b c) (d) (a b c d))
(append-to-form (a b c d) () (a b c d))

I would be interested in the specific mental steps required to carry out the rule matching.

Thank you in advance.

---

Play interpreter by taking a piece of paper and writing down every single step. For every step you write down which rule was/can be triggered and what variable was bound to what value.

For example:

(append-to-form (a b) (c d) ?z)

triggers the rule

(rule (append-to-form (?u . ?v) ?y (?u . ?z)) 
  (append-to-form ?v ?y ?z))

with

?u = a, ?v = (b), ?y = (c d), ?z = (a . ?z_2)

Note: ?z in the original query is supposed to be a different variable from ?z in the rule body, therefor rename the rule's ?z into ?z_2. A list (1 2 3) when matched to (?a . ?b) produces ?a = 1, ?b = (2 3) like when car/cdr'ing a list.

These bindings are applied to the body of the rule (append-to-form ?v ?y ?z) So we get

(append-to-form (b) (c d) ?z_2)

which again becomes

(append-to-form () (c d) ?z_3)

and triggers a different rule: (rule (append-to-form () ?y ?y)) binding ?z_3 to (c d). Then recursion kicks in, ?z_2 was defined as (b . ?z_3), ?z was defined as (a . ?z2)

The original query (append-to-form (a b) (c d) ?z) gets applied to the bindings in which ?z = (a . (b . (c d))) and returns (append-to-form (a b) (c d) (a b c d))

The rest of the exercises are left to the reader ;)

The crucial concepts here are pattern matching and unification which can be found at section 4.2.2. The whole query evaluator is really the most difficult piece in SICP, so don't be discourage. It is well worth the effort. Try to run the code (in an R5RS Scheme) and fiddle with it, such as adding tracing.