# 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’ <n> between trees. For instance, if I wanted to capture the notion of the symbol f being commutative and associative, I could write:

       f         f
<1>:  / \   =   / \     # commutativity f(ξ, ζ) = f(ζ, ξ)
(ξ) (ζ)   (ζ) (ξ)

f         f
/ \       / \
<2>:  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  <1>  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 <1> and <2>.


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
<1>:  / \  =  |
(n)  1   (n)

s       +
<2>: |  =   / \
+    (n)  s
/ \        |
(n)  (m)    (m)


Check this out:

            +
5 matches  / \  under {(ξ): 2}, because...
3  (ξ)
<1>          <2>
...5 = s(4) = s(s(3)) = s(+(3, 1)) = +(3, s(1)) = +(3, 2) which matches 5 with {(ξ): 2}.

(as trees:)
s   s  <1>  s  <2>   +       +                  +
...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!