Are there any efficient algorithms to decide whether two trees of limited depth, where all nodes have a finite number of childs, are equal interpreted as finite sets with the leaves the "atomic" elements?
The complication comes from that equality depends on membership and membership depends on equality so I guess the natural approach is recursion.
The answer depends on whether you have ordered or unordered trees. For ordered trees, the simplest algorithm that occurs to me is:
However, this won't work so well for unordered trees. The approach for that would be to create a 'tree certificate' or 'isomorphism code'. I'll describe the approach given in "Algorithms on Trees and Graphs" by Gabriel Valiente.
An isomorphism code is a sequence of numbers, starting from the root. It basically follows the same structure as the algorithm above, except that you sort the children of a node by their isomorphism codes in lex order.
For example, the code for the 4-star tree is [5, 1, 1, 1, 1] as there are four children of the root, so the root = [5] + [1, 1, 1, 1] with a [1] for each child. A linear tree on 5 nodes is [5, 4, 3, 2, 1] as the root has one child, which has one child, etc down to the leaf.