# How to prove the correctness of the binary tree inversion algorithm?

Define the inversion of a binary tree as the tree whose left sub-tree is a mirror reflection of the original tree's right sub-tree around the center and right sub-tree a mirror reflection of the original tree's left sub-tree.

Examples:

Inversion 1           Inversion 2

C    |    C           C    |    C
/ \   |   / \           \   |   /
A   B  |  B   A           B  |  B
/   |   \
A    |    A



Consider the following binary tree inversion algorithm (source: LeetCode):

/**
* Definition for a binary tree node.
* public class TreeNode {
*     int val;
*     TreeNode left;
*     TreeNode right;
*     TreeNode() {}
*     TreeNode(int val) { this.val = val; }
*     TreeNode(int val, TreeNode left, TreeNode right) {
*         this.val = val;
*         this.left = left;
*         this.right = right;
*     }
* }
*/
public TreeNode invertTree(TreeNode root) {
if (root == null) return null;
TreeNode tmp = root.left;
root.left = invertTree(root.right);
root.right = invertTree(tmp);
return root;
}


I sought to prove it inductively on the depth of tree but am stuck at the inductive step. How can I show that the mirror reflection of the left subtree (or right) around the center of the root tree is a combination of moving the subtree from root.right to root.left and inverting the subtree around the center of the subtree itself?

It might be surprising to you, but "the mirror reflection of the right subtree around the center of the root tree is a combination of moving the subtree from root.right to root.left and inverting the subtree around the center of the subtree itself" could be, in fact, part of the definition of "a mirror reflection of the right subtree around the center of the root tree"!

Note that the following definition of "the inversion of a binary tree", as given in the question, does not define what is the "mirror reflection of the original tree's right subtree". Although that mirroring is pretty intuitive for a human to understand accurately, given the accompanying illustrations, it is, in fact, not defined/specified clear enough to enable you to prove the correctness of the algorithm formally.

Define the inversion of a binary tree as the tree whose left subtree is a mirror reflection of the original tree's right subtree around the center and right subtree a mirror reflection of the original tree's left subtree.

So, here is the real question.

### How do we define mirror reflection formally?

Here is a recursive definition. (This can be seen as taking the given algorithm as the definition basically.)

Given a binary tree $$T$$ or an empty graph, its mirror reflection $$T'$$ is another graph such that

• $$T'$$ is empty if $$T$$ is empty.
• $$T'$$ is a single node that is the same as $$T$$'s single node if $$T$$ is a single node.
• Otherwise, $$T'$$ is also a binary tree such that
• the root of $$T'$$ is the same as the root of $$T$$ and
• the left subtree of $$T'$$ is a mirror reflection of the right subtree of $$T$$ and
• the right subtree of $$T'$$ is a mirror reflection of the left subtree of $$T$$.

When $$T'$$ is a mirror reflection of $$T$$, we also say $$T'$$ is a mirror reflection of $$T$$ along/around the center of $$T$$, or any imaginary line that goes from root to a leaf.

Here is a non-recursive definition, that is equivalent to the above.

Given a binary tree $$T$$ or an empty graph, its mirror reflection is any graph that is isomorphic to the graph $$T'$$ defined below.

• If $$T$$ is empty, so is $$T'$$.
• Otherwise, let $$V$$ be the nodes of $$T$$. Let $$V'$$ be a copy of $$V$$; that is, for each $$v\in V$$, there is unique node in $$V'$$ that corresponds to $$v$$. Call that unique node $$v'$$.
• For any two nodes $$p, c\in V$$ such that $$c$$ is the left child of $$p$$, we let $$c'$$ be the right child of $$p'$$.
• For any two nodes $$p, c\in V$$ such that $$c$$ is the right child of $$p$$, we let $$c'$$ be the left child of $$p'$$.

The OP also proposes the following geometric/graphical definition of "inversion of a tree".

Let $$(a,b)$$ be the coordinate of the node at depth $$a$$ that is the $$b$$-th node from the imaginary center line. If $$b$$ is negative then the node is to the left of the line. Then the inversion can be defined as the resulting tree if we map $$(a,b)$$ to $$(a,-b)$$ and keep the edges accordingly.

The definition above, although graphically clear to a human, might not be very friendly for rigorous reasoning. For example, "the b-th node from the imaginary center line" requires further non-trivial clarification.

With either of my definitions above, it will be rather easy to prove the correctness of the algorithm.

You might have noticed by now that inversion of a binary tree means exactly the same as its mirror reflection!

• Indeed, the key to this proof (as with many) is to formalize definitions Apr 22 at 13:46
• Thank you for formalizing this recursive definition for me! And what if I defined inversion as a mirror reflection along the imaginary center line formalized as follows: Let (a,b) be the coordinate of the node at depth a that is the b-th node from the imaginary center line. If b is negative then the node is to the left of the line. Then the inversion can be defined as a tree where (a,b) is mapped to (a,-b), and show this definition is equivalent to the one you formalized?
– Kun
Apr 23 at 3:50
• Using geometry/coordinates to describe graphs is a nice perspective. To enable a rigorous proof with mathematical rigor, we have to define the meaning of a node being "b nodes away from the imaginary center line". Once you have defined all terms using the basic terms that are considered as defined by convention, it will be easy to sort out definitions and to provide proofs to the "obvious" propositions we might have here. Apr 23 at 4:25
• In a similar vein, to provide a rigorous proof for Euler's formula on convex polyhedra also involves substantial work to clarify/define what is "a convex polyhedra", a concept that is so intuitively clear. You might be interested in Imre Lakatos's book Proofs and Refutations: The Logic of Mathematical Discovery. Apr 23 at 4:33
• Oh, yes, your definition of inversion by geometry/coordinate approach (with missing part clarified/defined) is equivalent to the one I formalized in my answer. Textually and logically, my definition is easier. Intuitively and graphically, your definition is attractive. Apr 23 at 6:37