The phase folding optimization is a circuit optimization used in many quantum compilers as a fast and effective way of reducing the number of high-cost gates in a quantum circuit. However, existing formulations of the optimization rely on an exact, linear algebraic representation of the circuit, restricting the optimization to being performed on straightline quantum circuits or basic blocks in a larger quantum program. We show that the phase folding optimization can be re-cast as an \emph{affine relation analysis}, which allows the direct application of classical techniques for affine relations to extend phase folding to quantum \emph{programs} with arbitrarily complicated classical control flow including nested loops and procedure calls. Through the lens of relational analysis, we show that the optimization can be powered-up by substituting other classical relational domains, particularly ones for \emph{non-linear} relations which are useful in analyzing circuits involving classical arithmetic. To increase the precision of our analysis and infer non-linear relations from gate sets involving only linear operations -- such as Clifford+$T$ -- we show that the \emph{sum-over-paths} technique can be used to extract precise symbolic transition relations for straightline circuits. Our experiments show that our methods are able to generate and use non-trivial loop invariants for quantum program optimization, as well as achieve some optimizations of common circuits which were previously attainable only by hand.

翻译：相位折叠优化是一种被众多量子编译器采用的电路优化技术，它通过快速有效的方式减少量子电路中高成本门的数量。然而，该优化现有的形式化方法依赖于对电路精确的线性代数表示，导致优化仅适用于直线型量子电路或大型量子程序中的基本块。本文证明，相位折叠优化可被重新表述为一种仿射关系分析，这使得经典仿射关系分析技术能够直接应用于扩展相位折叠优化至具有任意复杂经典控制流（包括嵌套循环和过程调用）的量子程序。通过关系分析的视角，我们证明该优化可通过替换其他经典关系域（特别是对分析涉及经典算术的电路非常有用的非线性关系域）来增强其能力。为了提高分析的精度并从仅包含线性操作（如Clifford+$T$）的门集合中推断非线性关系，我们证明路径求和技术可用于提取直线型电路的精确符号转移关系。实验结果表明，我们的方法能够为量子程序优化生成并利用非平凡的循环不变量，同时实现对常见电路的一些优化，这些优化此前仅能通过手动方式完成。