<p>The process you seem to be looking for (merging two descriptions of labeled trees) is called <a href="https://en.wikipedia.org/wiki/Unification_(computer_science)" rel="noreferrer">unification</a>. According to the linked Wikipedia article it can be solved in linear time.</p>

CC BY-SA 3.0
2017-05-22T08:49:57.973Z
For an extensive and understandable presentation of unification and its related algorithms, I would recommend the famous "All that" book : Franz Baader and Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press.
holf
CC BY-SA 3.0
2017-05-21T16:19:12.003Z
2017-05-21T16:19:12.003Z
David Eppstein
<p>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. </p>

<p>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.</p>

<p>In the following the "types" are numbers.</p>

<p><strong>Example 1:</strong></p>

<p><strong>A</strong> tree is</p>

<pre><code>1
|-2
|-a
</code></pre>

<p><strong>B</strong> tree is</p>

<pre><code>1
|-2
|-3
</code></pre>

<p>The solution is <code>a-&gt;3</code></p>

<p><strong>Example 2:</strong></p>

<p><strong>A</strong> tree is</p>

<pre><code>1
|-2
|-a
</code></pre>

<p><strong>B</strong> tree is</p>

<pre><code>1
|-3
|-3
</code></pre>

<p>This does not have a solution.</p>

<p><strong>Example 3:</strong></p>

<p><strong>A</strong> tree is</p>

<pre><code>1
|-2
|-a
</code></pre>

<p><strong>B</strong> tree is</p>

<pre><code>1
|-2
|-b
</code></pre>

<p>The solution is <code>a=b</code> (the equation is underdetermined so to say)</p>

CC BY-SA 3.0
2017-05-20T13:01:07.843Z
From your post it seems that the trees are *rooted* {i.e root 1 with child 2 and root 2 with child 1 are considered different trees} and that children are *ordered* {i.e that root 1 with children 2 and 3 and root 1 with children 3 and 2 are considered different}, please confirm.
daniello
CC BY-SA 3.0
2017-05-20T13:39:19.337Z
@daniello indeed that is true.
Adam
CC BY-SA 3.0
2017-05-20T15:04:44.743Z
In that case just doing a DFS in both trees simultaneously should do the trick, no?
daniello
CC BY-SA 3.0
2017-05-20T21:35:09.533Z
Isn't this just https://en.wikipedia.org/wiki/Unification_(computer_science) ?
David Eppstein
CC BY-SA 3.0
2017-05-21T06:51:21.303Z
@DavidEppstein looks like exactly what i was looking for
Adam
CC BY-SA 3.0
2017-05-21T16:19:08.177Z
Ok, I'll upgrade this from a comment to an answer.
David Eppstein
CC BY-SA 3.0
2017-06-01T18:55:41.197Z
It should be possible to sole in linear time however article on Wikipedia does not explain it to deeply
Brian Atkins
CC BY-SA 3.0
2017-06-05T05:43:12.053Z
The following is the basic description of unification.  You have a tree A and a tree B.  Both A and B contain variables which may represent numbers or entire subtrees.  You want to find a substitution for the variables of A and a substitution for the variables of B so that the two resulting trees are equivalent.  Now, maybe you don't just want any substitutions, but you want the "most general" substitutions that make the resulting trees equivalent.  I would be more than happy to talk further about this concept with you and provide more detail if it's something that you're interested in.
Michael Wehar
CC BY-SA 3.0
2017-06-05T05:52:54.897Z
I've implemented a few unification algorithms. I wrote one in JavaScript a while back.  Feel free to let me know if you're looking to implement something using unification.
Michael Wehar
<graph-algorithms><term-rewriting-systems>
Solving a "tree-equation"?
Adam
# Solving a "tree-equation"?

(Asked by: username_0 on 2017-05-20)

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->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)

**Tags:** graph-algorithms, term-rewriting-systems

> **Comments:**
> **username_1**: From your post it seems that the trees are *rooted* {i.e root 1 with child 2 and root 2 with child 1 are considered different trees} and that children are *ordered* {i.e that root 1 with children 2 and 3 and root 1 with children 3 and 2 are considered different}, please confirm.  
> **username_0**: @username_1 indeed that is true.  
> **username_1**: In that case just doing a DFS in both trees simultaneously should do the trick, no?  
> **username_2**: Isn't this just https://en.wikipedia.org/wiki/Unification_(computer_science) ?  
> **username_0**: @DavidEppstein looks like exactly what i was looking for  
> **username_2**: Ok, I'll upgrade this from a comment to an answer.  
> **username_3**: It should be possible to sole in linear time however article on Wikipedia does not explain it to deeply  
> **username_4**: The following is the basic description of unification.  You have a tree A and a tree B.  Both A and B contain variables which may represent numbers or entire subtrees.  You want to find a substitution for the variables of A and a substitution for the variables of B so that the two resulting trees are equivalent.  Now, maybe you don't just want any substitutions, but you want the "most general" substitutions that make the resulting trees equivalent.  I would be more than happy to talk further about this concept with you and provide more detail if it's something that you're interested in.  
> **username_4**: I've implemented a few unification algorithms. I wrote one in JavaScript a while back.  Feel free to let me know if you're looking to implement something using unification.  

---

## 1 answers

### Answer by username_2 on 2017-05-21. Score: 9 | Accepted answer

The process you seem to be looking for (merging two descriptions of labeled trees) is called [unification](https://en.wikipedia.org/wiki/Unification_(computer_science)). According to the linked Wikipedia article it can be solved in linear time.

> **Comments:**
> **username_5**: For an extensive and understandable presentation of unification and its related algorithms, I would recommend the famous "All that" book : Franz Baader and Tobias Nipkow (1998). Term Rewriting and All That. Cambridge University Press.  

---

