←Return to chapter

1.2. Contributions and thesis outline

Preliminaries #

The thesis starts in chapter 2 with a review of the main concepts on which the rest of the thesis is built. Aside from a short introduction to quantum computations (section 2.1) and a survey of the major quantum circuit optimisation techniques (section 2.2), this chapter makes two observations that impart a research direction to the rest of the thesis:

1. The emergence of hybrid quantum-classical computations is rendering the quantum circuit obsolete as the main representation of quantum computations within compilers (section 2.3).
2. The best optimisation outcomes will combine classical and quantum compiler optimisations. This can be achieved by adopting abstractions that are interoperable with classical compiler infrastructure (section 2.4).

A graph transformation formalism for quantum computations #

Chapters 3, 4, and 5 form the core of this thesis and present our main contributions. The results in chapter 3 are crucial stepping stones for the rest of the thesis. Chapters 4 and 5 meanwhile present our most significant contributions to the state of the art.

In chapter 3, we propose minIR, a new graph-based intermediate representation (IR) for quantum computations. MinIR is a minimal subset of the Hierarchical Unified Graph Representation (HUGR), recently presented in joint work Mark K., 2025Seyon Sivarajah, Alan Lawrence, Alec Edgington, Douglas Wilson, Craig Roy, Luca Mondada, Lukas Heidemann, Ross Duncan Mark Koch. 2025. HUGR: A Quantum-Classical Intermediate Representation. Retrieved (talk recording) from https://www.youtube.com/live/D8esZrt7ogk?feature=shared&t=5217 and the subject of ongoing development. It is to our knowledge the first compiler IR with support for linear types – required to model the restrictions that quantum mechanics imposes on quantum computations.

Unlike quantum circuits, minIR (and HUGR) programs can model computations that act on arbitrary combinations of classical (bits) and quantum data (qubits) within a single, unified representation. It represents the best of two worlds: it combines the safety guarantees of quantum-specific representations such as quantum circuits (i.e. it is impossible to declare physically unrealisable computations), whilst at the same time being interoperable with classical compiler IRs.

Graph-based representations of computations, known as computation graphs in deep learning and dataflow graphs within the compiler community, are common in these fields. Our original contribution is in the formalisation of the IR transformation semantics: whereas classical compilers typically define IR transformations in terms of the values that they depend on and the values that they overwrite, this approach implicitly relies on value copying and discarding and thus does not generalise to linear values. Instead, we define graph rewriting semantics on minIR and show sufficient conditions for which minIR transformations preserve the validity of the program, and in particular the linearity conditions.

The encoding of quantum computations as graphs sets the stage for quantum compilation and optimisation using graph transformation systems (GTS), in which the set of transformations that the compiler is allowed to perform is expressed by a set of graph transformation rules. This is in effect a generalisation of an approach first proposed in Xu, 2022Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar and Zhihao Jia. 2022. Quartz: Superoptimization of Quantum Circuits. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, June 2022. Association for Computing Machinery, 625--640. doi: 10.1145/3519939.3523433 in the context of quantum circuits. We improve on this work with two major contributions that resolve critical issues that concerning the scaling of the technique to large numbers of transformation rules and large inputs respectively.

Pattern matching #

Our first major contribution is a pattern matching algorithm, presented in chapter 4. The main result is a runtime complexity bound independent of the number of patterns being matched, achieved using a one-off pre-computation. This is to our knowledge the first pattern matching algorithm for quantum circuits that does not depend on the number of patterns. Whilst similar multi-pattern matching techniques have been explored in other domains such as RETE networks Forgy, 1982Charles L. Forgy. 1982. Rete: A fast algorithm for the many pattern/many object pattern match problem. Artificial Intelligence 19, 1 (Septempter 1982, 17--37). doi: 10.1016/0004-3702(82)90020-0 Varró, 2013Gergely Varró and Frederik Deckwerth. 2013. A Rete Network Construction Algorithm for Incremental Pattern Matching Ian, 2003Wright Ian and James A. R. Marshall. 2003. The execution kernel of RC++: RETE*, a faster RETE with TREAT as a special case. International Journal of Intelligent Games and Simulation 2, 1 (Feb 2003, 36-48) and computational biology Danos, 2007Vincent Danos, Jérôme Feret, Walter Fontana and Jean Krivine. 2007. Scalable Simulation of Cellular Signaling Networks Boutil., 2017Pierre Boutillier, Thomas Ehrhard and Jean Krivine. 2017. Incremental Update for Graph Rewriting, no algorithm is known with provable sub-exponential worst-case complexity. These results were published in Mondada, 2025Luca Mondada and Pablo Andrés-Martínez. 2025. Scalable Pattern Matching in Computation Graphs. Electronic Proceedings in Theoretical Computer Science 417 (March 2025, 71--95). doi: 10.4204/eptcs.417.5.

The proved complexity bound applies to computations with only linear values¹, of which quantum circuits are a special case. The result is expressed in terms of maximal pattern width $w$ and depth $d$, two measures of pattern size defined in section 4.2. The main result, presented in Proposition ., is reproduced here:

The runtime complexity is dominated by an exponential scaling in maximal pattern width $w$. Meanwhile, the advantage of our approach over matching one pattern at a time grows with the number of patterns $\ell$. It is thus of particular interest for matching numerous small width patterns.

We illustrate this point by comparing our approach to a standard algorithm that matches one pattern at a time Jiang, 1998Xiaoyi Jiang and Horst Bunke. 1998. Marked subgraph isomorphism of ordered graphs. In Advances in Pattern Recognition, Berlin, Heidelberg. Springer Berlin Heidelberg, 122--131. doi: 10.1007/bfb0033230, with runtime complexity $O(\ell \cdot |P| \cdot |G|)$. Using $|P| \leq w\cdot d$ (cf. section 4.2), and comparing to eq. (1), we thus have a speedup in the regime $\Theta(c^w / w^{3/2}) < \ell$. On the other hand, $\ell$ is upper bounded by the maximum number $N_{w, d}$ of patterns of bounded width and depth. Using a crude lower-bound for $N_{w,d}$ derived in Appendix , we obtain a computational advantage for our approach when

In the case of quantum circuits, the width of the patterns is given by the number of qubits. The low-qubit regime where our approach shines coincides exactly with the typical applications of GTSs in quantum compilation: in Xu, 2022Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar and Zhihao Jia. 2022. Quartz: Superoptimization of Quantum Circuits. In Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, June 2022. Association for Computing Machinery, 625--640. doi: 10.1145/3519939.3523433 and Xu, 2023Amanda Xu, Abtin Molavi, Lauren Pick, Swamit Tannu and Aws Albarghouthi. 2023. Synthesizing Quantum-Circuit Optimizers. Proceedings of the ACM on Programming Languages 7, PLDI (June 2023, 835--859). doi: 10.1145/3591254, all rules used have at most 4 qubits.

We present benchmarks on a real world dataset of 10,000 quantum circuits in section 4.7, showing a 20x speedup over a leading C++ implementation of pattern matching for quantum circuits.

Confluently persistent graph rewriting #

Our second major contribution, in chapter 5, uses a well-known construction in GTSs, the unfolding Baldan, 1999Paolo Baldan, Andrea Corradini and Ugo Montanari. 1999. Unfolding and Event Structure Semantics for Graph Grammars. In Foundations of Software Science and Computation Structures, Berlin, Heidelberg. Springer Berlin Heidelberg, 73--89. doi: 10.1007/3-540-49019-1_6, to derive a novel data structure $\mathcal{D}$ that compresses the representation of the space $\mathcal{G}$ of all graphs reachable from an input within a GTS. We call $\mathcal{D}$ the factorised search space of $\mathcal{G}$. Optimisation problems over the space of reachable graphs in a GTS can then equivalently be expressed as optimisation problems over $\mathcal{D}$.

We show in section 5.5 that under some assumptions on the GTS and input, there is an exponential complexity separation in the input size between the size of the factorised search space $\mathcal{D}$ – which admits an asymptotically linear upper bound – and the size of the rewrite space $\mathcal{G}$ that it encodes – which grows at least exponentially.

$\mathcal{D}$ is furthermore the first confluently persistent data structure Drisco., 1994James R. Driscoll, Daniel D. K. Sleator and Robert E. Tarjan. 1994. Fully persistent lists with catenation. Journal of the ACM 41, 5 (Septempter 1994, 943--959). doi: 10.1145/185675.185791 Fiat, 2003Amos Fiat and Haim Kaplan. 2003. Making data structures confluently persistent. Journal of Algorithms 48, 1 (August 2003, 16--58). doi: 10.1016/s0196-6774(03)00044-0 [?] it performs non-destructive rewrites on immutable graph objects by maintaining an explicit history of all graph rewrites and their dependencies. This allows concurrent application of multiple rewrites and can merge rewritten graphs that were obtained independently. This represents an exciting development in its own right that opens the door to functional programming and massively parallelised approaches to graph rewriting (see section 6.2).

The intuition behind the exponential reduction in search space size is as follows: if rewrites $r_1, \dots, r_n$ apply to disjoint subgraphs of a common graph $G$, then $\mathcal{D}$ will be of size $n$, storing the set possible rewrites, rather than the up to $2^n$ distinct graphs in $\mathcal{G}$ obtained by applying a subset of the rewrites. To generalise to arbitrary rewrites, the data structure $\mathcal{D}$ must keep track of the dependencies and overlaps between rewrites and update these as more rewrites are added to $\mathcal{D}$.

A lot of parallels can be drawn between this approach and equality saturation, a technique for term rewriting with applications in classical compilers. We explore these connections in section 5.2.

Unlike the results of chapter 4, the construction and bounds proven in chapter 5 can be applied to a wide range of graph rewriting domains. It has particularly significant implications for applications of GTSs that are unable to derive rewriting strategies from first principles, and hence have to resort to an exhaustive (or heuristic) exploration of the rewrite space $\mathcal{G}$. They can proceed as follows:

1. Exploration phase. Construct the factorised search space $\mathcal{D}$ by finding and applying rewrites, in time proportional to $|\mathcal{D}|$. With our results, this results in an exponential speedup over the naive exploration of $\mathcal{G}$ (section 5.3).

2. Extraction phase. Unlike the case of $\mathcal{G}$ where the optimal solution is an element $G_{opt} \in \mathcal{G}$, constructing the optimal solution $\mathcal{D} \rightarrow G_{opt}$ in $\mathcal{D}$ is a non-trivial extraction problem. We show in section 5.4 that the extraction can be expressed as a boolean satisfiability (SAT) problem; depending on the cost function, the optimisation can then be encoded as a side condition on SAT or by a generalisation of the problem to Satisfiability Modulo Theories (SMT).

In the worst case, SAT and SMT problems will require exponential time to solve Cook, 1971Stephen A. Cook. 1971. The complexity of theorem-proving procedures. In Proceedings of the third annual ACM symposium on Theory of computing - STOC ’71. ACM Press, 151--158. doi: 10.1145/800157.805047 Moskew., 2001Matthew W. Moskewicz, Conor F. Madigan, Ying Zhao, Lintao Zhang and Sharad Malik. 2001. Chaff: engineering an efficient SAT solver. In Proceedings of the 38th conference on Design automation - DAC ’01. ACM Press, 530--535. doi: 10.1145/378239.379017 Biere, 2021Armin Biere, Marijn J. H. Heule, Hans Maaren and Toby Walsh. 2021. Handbook of satisfiability (Second edition ed.). IOS Press, Amsterdam, thus cancelling the exponential compression of the search space $\mathcal{G} \rightarrow \mathcal{D}$. However, SAT and SMT are standardised problems for which heavily optimised solvers and optimisers have been developed Moura, 2008Leonardo de Moura and Nikolaj Bjørner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems. Springer Berlin Heidelberg, 337--340. doi: 10.1007/978-3-540-78800-3_24 Sebast., 2015Roberto Sebastiani and Patrick Trentin. 2015. OptiMathSAT: A Tool for Optimization Modulo Theories. In Computer Aided Verification. Springer International Publishing, 447--454. doi: 10.1007/978-3-319-21690-4_27. We expect that the instances of SAT and SMT that encode the extraction problem will scale well in practice:

• Clauses in the problem encode local properties that SAT solvers are well-suited to solve Zulkos., 2018Edward Zulkoski. 2018. Understanding and Enhancing CDCL-based SAT Solvers​: the boolean variables represent rewrites, which only impose restrictions on other rewrites that apply in the same neighbourhood of the graph.
• Furthermore, in quantum compilation applications, $\mathcal{D}$ can be sparsified: most rewrties in $\mathcal{D}$ do not change the cost function (think of IR transformations that reorder operations but do not reduce the runtime) and thus do not need to be encoded in the SAT problem.

In a first exploratory analysis, we present some empirical results that support our claims: by searching over the factorised search space instead of the naive search space, the optimiser is able to find the global optimum for circuits that are twice as large. Our results also exhibit a linear scaling in the size of the factorised search space, confirming that the approach should scale well to larger problems.

Conclusion #

The thesis concludes in chapter 6 with a discussion on how our contributions serve our overall goal of a scalable and modular quantum compiler platform. We discuss in particular two extensions of our work that we see as particularly promising: the generalisation of fast multi-pattern matching to non-linear values and to the persistent data structure $\mathcal{D}$ of chapter 5 (section 6.1) and the deployment of confluently persistent graph rewriting to a massively parallel distributed compute architecture (section 6.2).

←Return to chapter