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

Question

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.

Unification means providing a substitution such that the two expressions become the same. Substituting `q` with `pod` makes them the same. — Scott Hunter, Sep 08 '22 at 16:16
What does "works through list structure" mean? Any other *what*s? — Scott Hunter, Sep 08 '22 at 16:18
Unification understands how lists work so it can match variables and symbols at the same index with each other? — Alper, Sep 08 '22 at 16:22
I don't think the book makes that clear before in any way. But okay. Thanks! — Alper, Sep 08 '22 at 16:38
that's `q` (a variable) and `'pod` (a symbol datum used as a value). — Will Ness, Sep 12 '22 at 15:34

score 1 · Accepted Answer · answered Sep 12 '22 at 20:02

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.

"The double parenthesizing has no special meaning at all." So just a red herring of which there are a bunch in the book. — Alper, Sep 12 '22 at 22:26
yes, certainly. their examples are all over the place, _not_ to the point quite often. — Will Ness, Sep 12 '22 at 22:49

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

1 Answers1