The term "commuting conversions" in proof theory refers to a proof transformation of natural deduction proofs that involve sums (disjunction and existential formulae).
The motivation for these comes from a desirable equivalence relation among natural deduction proofs that is lost when $\vee$ and $\exists$ are added.
\(\newcommand{\orelim}[0]{\color{blue}{(\vee{\mathrm{\small ELIM}})}}\)
Consider the following natural deduction rules
$$ \cfrac{\begin{array}[cc]{} \\ {} \\ A \vee B \end{array} \quad \begin{array}[cc]{} [A] \\ ~~\vdots \\ \phantom{[}C\phantom{]} \end{array}\quad
\begin{array}[cc]{}
[B] \\
~~\vdots \\
\phantom{[}C\phantom{]}
\end{array}
}
{C}~\color{blue}{(\vee{\mathrm{\small ELIM}})} $$
$$ \cfrac{\begin{array}[cc]{} \\ {} \\ \exists x . (x)\end{array} \quad \begin{array}[c]{} [P(t)] \\ ~~\vdots \\ \phantom{[}C\phantom{]} \end{array}}
{C}~\color{blue}{(\exists{\mathrm{\small ELIM}})} $$
When the formula $C$ is not the end of the proof, but there is another formula $W$ that is derived, then we get
multiple proofs to derive the same thing.
These multiple proofs of the same thing are all
normal in the sense that there are no "detours" in the form of implication introduction and elimination. If we want a
normal form to be unique, then we must necessarily pick one among these possible proof and designate it as "normal." This happens by adding additional conversions.
$$ \cfrac{\begin{array}[cc]{} \\ {} \\ A \vee B \end{array} \quad \begin{array}[cc]{} [A] \\ ~~\vdots \\ \phantom{[}C\phantom{]} \end{array}\quad
\begin{array}[cc]{}
[B] \\
~~\vdots \\
\phantom{[}C\phantom{]}
\end{array}
}
{\cfrac{~C~}{~W~}}
~ \rightsquigarrow ~
%
\cfrac{\begin{array}[cc]{} \\ {} \\ A \vee B \end{array} \quad \begin{array}[cc]{} [A] \\ ~~\vdots \\ \phantom{[}C\phantom{]} \\ \hline \phantom{[}W\phantom{]} \end{array}\quad
\begin{array}[cc]{}
[B] \\
~~\vdots \\
\phantom{[}C\phantom{]} \\
\hline \phantom{[}W\phantom{]}
\end{array}
}
{W}$$
$$ \cfrac{\begin{array}[cc]
{} & [P(t)] \\
{} & \vdots \\
\exists x . P(x) & C \\
\end{array}}{\cfrac{~C~}{~W~}}
~ \rightsquigarrow ~
\cfrac{\begin{array}[cc]
{} & [P(t)] \\
{} & \vdots \\
{} & C \\
\exists x . P(x) & \overline{~W~} \\
\end{array}}{W}
$$
Pattern matching example
Programmers may appreciate the following presentation of the same thing in Scala-like syntax. This:
$\color{blue}{W}$($r$ match { case Left(a) => $\color{blue}{s}$; case Right(b) => $\color{blue}{t}$ })
is the same as this:
$r$ match { case Left(a) => $\color{blue}{W(s)}$; case Right(b) => $\color{blue}{W(t)}$ })
