Frame 1:33 - How do we unify two lists?

I don't think it's been written anywhere how this is supposed to work.

We get:

(run* q
  (==
    '( ((pea)) pod)
    `( ((pea)) ,q)))

In the quasiquote form pea is quoted so remains the symbol and q is unquoted so refers to the variable in run. Then q seemingly becomes pod.

How are these two lists then unified with each other? What's the mechanism behind that? Can I just superimpose two lists on each other and then say that the elements at index 1 become the same?

Also still a mystery why pea is double parensed.

Solution

The unification goal

 (==
    '( ((pea)) pod)
    `( ((pea)) ,q))

is the same as

  (==
    (list (list (list 'pea)) 'pod)
    (list (list (list 'pea))  q  ))

so yes, it is "working through list structure", and no other kinds of structures -- just lists. This should be straightforward and plain enough to code by recursively going along the two lists in unison as long as the structure is the same and the sub-terms can be unified.

So the above goal succeeds, extending its argument substitution with the pairing of the variable q and its value, the symbol datum 'pod. But also,

  (==
    (list (list p          ) 'pod)
    (list (list (list 'pea)) q   ))

would also succeed, extending its argument substitution with the pairing of the variable q the symbol 'pod as well as the pairing of the variable p with its value, (list 'pea) -- provided that p and q were indeed defined as logical variables, by run* or by fresh. Whereas

  (==
    (list (list "p"        ) 'pod)
    (list (list (list 'pea)) q   ))

would fail.

The double parenthesizing has no special meaning at all.