Solving a "tree-equation"? Given two trees A and B, each of their nodes except some leaves have a "type" (which also determines the number of children, the node has, having that type). The leaves which don't have a type are identified by letters (variables) (a,b,c,...). Each letter may occur multiple times in a tree. 

The task is to devise an algorithm to 'solve' the 'equation' A=B, i.e. assign trees to the variables (possibly containing other variables). One tree (x) equals to an other (y) iff x and y are the same variables or the root of both have the same type and their respective children are equal.

In the following the "types" are numbers.

Example 1:

A tree is

1
|-2
|-a


B tree is

1
|-2
|-3


The solution is a-&gt;3

Example 2:

A tree is

1
|-2
|-a


B tree is

1
|-3
|-3


This does not have a solution.

Example 3:

A tree is

1
|-2
|-a


B tree is

1
|-2
|-b


The solution is a=b (the equation is underdetermined so to say)
The process you seem to be looking for (merging two descriptions of labeled trees) is called unification. According to the linked Wikipedia article it can be solved in linear time.