patternMinor

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

Submitted by: @import:stackexchange-cs·Mar 10, 2026·

Viewed 0 times

goaldirectedunificationtreesbetweenpatternseekingmatching

Problem

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’ ` between trees. For instance, if I wanted to capture the notion of the symbol f

 being commutative and associative, I could write:

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

        f         f
       / \       / \
:  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    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
/ \

Solution

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.

Context

StackExchange Computer Science Q#91240, answer score: 3

Revisions (0)

No revisions yet.