E-Unification: “Goal seeking” pattern matching between directed trees Preamble

Suppose we have some symbols x, y, ... and wildcards (ξ), (ζ), ... which have any meaning. Wildcards are said to ‘match’ any symbol: wildcard (ξ) matches symbol x under the mapping {(ξ): x}. Now suppose we can construct directed trees from these symbols and wildcards. The notion of matching should extend to these trees, like this:

  x                 x       
 / \               / \      
a   y   matches  (ξ)  y   under the mapping {(ξ): a, (ζ): b}.
   / \               / \    
  z   b             z  (ζ)  


It is easy to implement an algorithm which takes two trees like those above and gives the necessary mapping. (Does it have a name?)

I want to introduce certain ‘equivalence relations’ &lt;n&gt; between trees. For instance, if I wanted to capture the notion of the symbol f being commutative and associative, I could write:

       f         f
&lt;1&gt;:  / \   =   / \     # commutativity f(ξ, ζ) = f(ζ, ξ)
    (ξ) (ζ)   (ζ) (ξ)

        f         f
       / \       / \
&lt;2&gt;:  f  (χ) = (ξ)  f   # associativity f(f(ξ, ζ), χ) = f(ξ, f(ζ, ξ))
     / \           / \
   (ξ) (ζ)       (ζ) (χ)


This is where things get interesting, because I now want to implement a more intelligent matching algorithm which, given a set of equivalence relations like those above, is able to perform ‘indirect’ matches like this:

  f                          f          
 / \  (indirectly) matches  / \  under the mapping {(ξ): x}...
y   x                     (ξ)  y                     

                f  &lt;1&gt;  f                            f
   ...because  / \  =  / \  which directly matches  / \ .
              y   x   x   y                       (ξ)  y


Question

How would one go about finding an algorithm which is able to transform a given tree (via given rules) so that it ‘matches’ another tree?

Is there a name for this kind of problem?



More examples

Matches aren’t always unique. Ideally, the algorithm should be able to find all of them.

   f                 f
  / \               / \
 x   f   matches   f  (ξ)  under {(ξ): y, (ζ): z} or {(ξ): z, (ζ): y}...
    / \           / \
   y   z        (ζ)  x

         ...using rules &lt;1&gt; and &lt;2&gt;.


A quintessential demonstrative example:

For brevity, define the symbols 1, 2, 3, ... in terms of 0 and a unary symbol s:

1 = s(0), 2 = s(s(0)), 3 = s(s(s(0)))...


Now, define two transformation rules s(n) = +(n, 1) and s(+(n, m)) = +(n, s(m)):

       +      s
&lt;1&gt;:  / \  =  |
    (n)  1   (n)

     s       +
&lt;2&gt;: |  =   / \
     +    (n)  s
    / \        |
  (n)  (m)    (m)


Check this out:

            +
5 matches  / \  under {(ξ): 2}, because...
          3  (ξ)
                     &lt;1&gt;          &lt;2&gt;
...5 = s(4) = s(s(3)) = s(+(3, 1)) = +(3, s(1)) = +(3, 2) which matches 5 with {(ξ): 2}.

   (as trees:)
       s   s  &lt;1&gt;  s  &lt;2&gt;   +       +                  +
...5 = | = |   =   |   =   / \  =  / \  which matches / \  with {(ξ): 2}.
       4   s       +      3   s   3   2              3  (ξ)
           |      / \         |
           3     3   1        1




(I apologise for the size of this question. I don’t have a background, so feel free to improve this post.)

Perhaps you can direct me to some reading, or set me off in the right direction? Thanks heaps!
This is called unification.  There is a one-to-one correspondence between terms and trees; the tree is the parse tree of a corresponding term.  It sounds like you want the most general unifier.  There are standard algorithms for solving this.  However, this doesn't handle equivalence relations like commutativity or associativity.  E-unification might be what you are looking for.