Chapter 5

Fully and Confluently Persistent Graph Rewriting

This chapter leverages another construction from graph rewriting theory that finds a direct application in quantum compilation: the unfolding of graph transformation systems 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 Winskel, 1987Glynn Winskel. 1987. Event structures. Whereas most applications to date have focused on using unfolding for model verification (see section 5.1 for a review), we will use the same techniques to instead speed up optimisation problems over the space of reachable graphs in a GTS.

In the unfolding, graph rewrites are expressed as persistent modifications of the graph. Mutable data structures are typically ephemeral: modifying the data structure overwrites information and invalidates any references to the old data. In contrast, a persistent data structure applies changes to the data so that both the old and new versions remain accessible – a famous example of this are version control systems such as git.

A data structure is fully persistent if modifications can be applied not only to the latest version but also to previous versions of the data structure. In that case, a version of the data may be used to create several new versions. Instead of a linear edit history of all mutations, the result is an edit history tree, with possibly many “most recent” versions – leaves in the edit history.

Finally, a fully persistent data structure is also confluently persistent if different versions of the data in the edit history can be joined together. As a result, the edit history forms a directed acyclic graph (DAG) of versions of the data, linked by data mutation and joining operations. Adopting terminology from git, we call a join of two or more versions a merge of multiple versions.

In this chapter, we will consider all graphs to be hypergraphs $(V, E)$ with vertex set $V$ and hyperedge set $E \subseteq V^\ast$. All results can easily be adapted to accommodate graph attributes, weights, and types as required by applications. This means the data structure and algorithms we present apply directly to minIR graphs and, more broadly, to most instances of graph rewriting.

The central object of study in this chapter is the graph rewrite. We restate a simplified version of Definition . here. We opt for convenience for a rewrite definition that omits the edge deletion set $E^-$ of Definition .. This is not a restriction of the general case, as can be seen by adding a “dummy” vertex $v_e$ for each edge $e$ in a graph: a rewrite that removes an edge $e \in E^-$ can equivalently be expressed by the rewrite that removes the dummy vertex $v_e \in V^-$¹.

As in previous chapters, $\sqcup$ denotes disjoint union, $f: A \rightharpoonup B$ denotes a partial function and $dom$ denotes the domain of definition of a (partial) function.

Define the context subgraph $G_C$ as the subgraph induced by the vertices

The rewritten graph resulting from applying $r$ to $G$ is the glueing

obtained from the union of $G_C$ and $G_R$ by merging all vertices within the same class in the equivalence relation $\sim_\mu$ that is the closure of $\mu$. We refer to section 3.5 for more details and an illustration of glueings and rewrites.

In this chapter, we will consider sequences of multiple rewrites. We will use the notation $V(G)$ and $E(G)$ to designate the vertices, respectively the edges, of a graph $G$. It is further assumed that the vertices $V(G)$ and $V(G')$ for $G \neq G'$ are always disjoint, a fact that we underline by always writing unions of graphs and vertices with $\sqcup$.

We make use of the fact that for every rewrite $r = (G_R, V^-, \mu)$, the equivalence classes $\alpha$ of $\sim_\mu$ are of the form

for some $m \in V(G_R)$. For every set of merged vertices $\alpha \subseteq V(G)$ in $r(G)$, there is thus a unique vertex not in $V^-$:

We choose to always identify the merged vertex in $r(G)$ with $m$. Using this convention, the set of vertices of $r(G)$ is simply

5.1. Related work

The unfolding of a graph transformation system (GTS) was first proposed in 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 as a generalisation of a well-known construction on Petri nets Winskel, 1987Glynn Winskel. 1987. Event structures. Originally defined for DPO rewriting, the unfolding was later generalised to SPO Baldan, 2007Paolo Baldan, Andrea Corradini, Ugo Montanari and Leila Ribeiro. 2007. Unfolding semantics of graph transformation. Information and Computation 205, 5 (May 2007, 733--782). doi: 10.1016/j.ic.2006.11.004 Baldan, 2014Paolo Baldan, Andrea Corradini, Tobias Heindel, Barbara König and Paweł Sobociński. 2014. Processes and unfoldings: concurrent computations in adhesive categories. Mathematical Structures in Computer Science 24, 4 (June 2014). doi: 10.1017/s096012951200031x and SqPO Behr, 2019Nicolas Behr. 2019. Sesqui-Pushout Rewriting: Concurrency, Associativity and Rule Algebra Framework. Electronic Proceedings in Theoretical Computer Science 309 (December 2019, 23--52). doi: 10.4204/eptcs.309.2 in arbitrary adhesive categories. The unfolding is a powerful GTS technique that has found applications in model verification Baldan, 2008Paolo Baldan, Andrea Corradini and Barbara König. 2008. Unfolding Graph Transformation Systems: Theory and Applications to Verification Baldan, 2008Paolo Baldan, Andrea Corradini and Barbara König. 2008. A framework for the verification of infinite-state graph transformation systems. Information and Computation 206, 7 (July 2008, 869--907). doi: 10.1016/j.ic.2008.04.002 Costa, 2012Simone André da Costa and Leila Ribeiro. 2012. Verification of graph grammars using a logical approach. Science of Computer Programming 77, 4 (April 2012, 480--504). doi: 10.1016/j.scico.2010.02.006 and other formal analysis tools such as model-based diagnosis Baldan, 2008Paolo Baldan, Thomas Chatain, Stefan Haar and Barbara König. 2008. Unfolding-Based Diagnosis of Systems with an Evolving Topology and model transformation analysis Bisztr., 2009Dénes András Bisztray. 2009. Compositional verification of model-level refactorings based on graph transformations. PhD Thesis. University of Leicester.

Unfoldings of finite GSTs are often infinite. A lot of work has therefore concerned itself with finding sufficient conditions for finiteness or the existence of finite complete prefixes of unfoldings Baldan, 2008Paolo Baldan, Andrea Corradini and Barbara König. 2008. Unfolding Graph Transformation Systems: Theory and Applications to Verification Baldan, 2004Paolo Baldan, Andrea Corradini and Barbara König. 2004. Verifying Finite-State Graph Grammars: An Unfolding-Based Approach. In CONCUR 2004 - Concurrency Theory, Berlin, Heidelberg. Springer Berlin Heidelberg, 83--98. doi: 10.1007/978-3-540-28644-8_6 Baldan, 2008Paolo Baldan, Andrea Corradini, Barbara König and Stefan Schwoon. 2008. McMillan's Complete Prefix for Contextual Nets Baldan, 2010Paolo Baldan, Alessandro Bruni, Andrea Corradini, Barbara König and Stefan Schwoon. 2010. On the Computation of McMillan's Prefix for Contextual Nets and Graph Grammars. In Graph Transformations, Berlin, Heidelberg. Springer Berlin Heidelberg, 91--106. doi: 10.1007/978-3-642-15928-2_7 Schwoon, 2013Stefan Schwoon. 2013. Efficient verification of sequential and concurrent systems. PhD Thesis. École normale supérieure de Cachan-ENS Cachan. On the other hand, unfoldings of GTSs of quantum computation are expected to be intractably large Yang, 2021Yichen Yang, Mangpo Phitchaya Phothilimtha, Yisu Remy Wang, Max Willsey, Sudip Roy and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. CoRR abs/2101.01332. doi: 10.48550/ARXIV.2101.01332, with no complete prefixes in general. Rather, our interests lie in finding heuristics that determine the subspace of the unfolding of interest, combined with fast algorithms to expand finite unfolding prefixes into larger ones. This chapter is to our knowledge the first work in this direction.

Persistent data structures on the other hand have a rich history in computer science Drisco., 1989James R. Driscoll, Neil Sarnak, Daniel D. Sleator and Robert E. Tarjan. 1989. Making data structures persistent. Journal of Computer and System Sciences 38, 1 (February 1989, 86--124). doi: 10.1016/0022-0000(89)90034-2 Lagogi., 2005George Lagogiannis, Yannis Panagis, Spyros Sioutas and Athanasios Tsakalidis. 2005. A survey of persistent data structures. In Proceedings of the 9th WSEAS International Conference on Computers, Stevens Point, Wisconsin, USA. World Scientific and Engineering Academy and Society (WSEAS), and particularly within functional programming Okasaki, 1996Chris Okasaki and Peter Lee. 1996. Purely functional data structures. Carnegie Mellon University, USA Okasaki, 1998Chris Okasaki and Andy Gill. 1998. Fast Mergeable Integer Maps. In Workshop on ML, Septempter 1998, 77--86 Hinze, 2005Ralf Hinze and Ross Paterson. 2005. Finger trees: a simple general-purpose data structure. Journal of Functional Programming 16, 02 (November 2005, 197). doi: 10.1017/s0956796805005769. Confluently persistent data structures were first explored in 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. A general treatment of the approach was subsequently presented in 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 and improved in Collet., 2012Sébastien Collette, John Iacono and Stefan Langerman. 2012. Confluent Persistence Revisited. In Proceedings of the Twenty-Third Annual ACM-SIAM Symposium on Discrete Algorithms, January 2012. Society for Industrial and Applied Mathematics, 593--601. doi: 10.1137/1.9781611973099.50. Chaler., 2018Parinya Chalermsook, Mayank Goswami, László Kozma, Kurt Mehlhorn and Thatchaphol Saranurak. 2018. Multi-Finger Binary Search Trees. In International Symposium on Algorithms and Computation 2018. Schloss Dagstuhl – Leibniz-Zentrum für Informatik. doi: 10.4230/LIPICS.ISAAC.2018.55 proposed a data structure for confluently persistent tries.

Within the field of graph transformations, there is a well-developed theory for persistent (and confluently persistent) transformations in the form of the concurrent graph transformation formalism of Corradini et al. Corrad., 1996A. Corradini, U. Montanari and F. Rossi. 1996. Graph Processes. Fundamenta Informaticae 26, 3,4 (241--265). doi: 10.3233/fi-1996-263402 and Baldan et al. Baldan, 1999Paolo Baldan, Andrea Corradini, Ugo Montanari, Francesca Rossi, Hartmut Ehrig and Michael Löwe. 1999. Concurrent Semantic of Algebraic Graph Transformations. In Handbook of Graph Grammars and Computing by Graph Transformation, August 1999. World Scientific, 107--187. doi: 10.1142/9789812814951_0003. This categorical formalism has also been extended to include support for overlapping transformations in Echahed, 2017Rachid Echahed and Aude Maignan. 2017. Parallel Graph Rewriting with Overlapping Rules. In Proceedings of the 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, LPAR, 300--318. doi: 10.29007/576h.

The first practical application of persistent graph rewriting was developed by the graph rewriting engine GRAPE Weber, 2017Jens H. Weber. 2017. GRAPE – A Graph Rewriting and Persistence Engine. In Graph Transformation. Springer International Publishing, 209--220. doi: 10.1007/978-3-319-61470-0_13 and was originally based on ephemeral data structures with transactional ACID semantics. Later, its successor, GrapeVine Weber, 2022Jens H. Weber. 2022. Tool Support for Functional Graph Rewriting with Persistent Data Structures - GrapeVine. In Graph Transformation. ICGT 2022. Springer International Publishing, 195--206. doi: 10.1007/978-3-031-09843-7_11, enhanced this with the first fully persistent data structure for graph rewriting. In this work, the vertices and edges that result from graph rewrites are stored individually in a specialised database. Depending on the requested data version, the graph can be retrieved from the database’s individual vertex and edge entities using the database’s graph query language. To our knowledge, no confluently persistent data structure has been proposed for graph rewriting.

As we will see in section 5.5, confluent persistence is a particularly valuable property in the absence of a rewriting strategy, i.e. a procedure to select and prioritise among possible graph transformations Echahed, 2008Rachid Echahed. 2008. Inductively Sequential Term-Graph Rewrite Systems. In Graph Transformations, ICGT. Springer Berlin Heidelberg, 84--98. doi: 10.1007/978-3-540-87405-8_7. This distinguishes the approach presented in this thesis from most previous work. Rewriting strategies feature prominently in PORGY, a tool for port graph rewriting Andrei, 2011Oana Andrei, Maribel Fernández, Hélène Kirchner, Guy Melançon, Olivier Namet and Bruno Pinaud. 2011. PORGY: Strategy-Driven Interactive Transformation of Graphs. Electronic Proceedings in Theoretical Computer Science 48 (February 2011, 54--68). doi: 10.4204/eptcs.48.7 Ferná., 2010Maribel Fernández and Olivier Namet. 2010. Strategic programming on graph rewriting systems. Electronic Proceedings in Theoretical Computer Science 44 (December 2010, 1--20). doi: 10.4204/eptcs.44.1; the graph rewriting software GROOVE provides the notion of a control program to govern the transformation order Rensink, 2004Arend Rensink. 2004. The GROOVE Simulator: A Tool for State Space Generation. In Applications of Graph Transformations with Industrial Relevance. Springer Berlin Heidelberg, 479--485. doi: 10.1007/978-3-540-25959-6_40; and finally, tools such as GrGen provide advanced control flow primitives to specify rewrite rule execution Geiß, 2006Rubino Geiß, Gernot Veit Batz, Daniel Grund, Sebastian Hack and Adam Szalkowski. 2006. GrGen: A Fast SPO-Based Graph Rewriting Tool. In Graph Transformations. ICGT 2006.. Springer Berlin Heidelberg, 383--397. doi: 10.1007/11841883_27.

Specifying rewriting strategies yields efficient graph transformation procedures and is particularly effective for systems with provable properties such as confluence and termination Verma, 1995Rakesh M. Verma. 1995. Transformations and confluence for rewrite systems. Theoretical Computer Science 152, 2 (December 1995, 269--283). doi: 10.1016/0304-3975(94)00255-0. As a result, rewriting strategies have also been used successfully within classical compiler optimisations Assmann, 2000Uwe Assmann. 2000. Graph rewrite systems for program optimization. ACM Transactions on Programming Languages and Systems 22, 4 (July 2000, 583--637). doi: 10.1145/363911.363914 and quantum circuit optimisation Fagan, 2018Andrew Fagan and Ross Duncan. 2018. Optimising Clifford Circuits with Quantomatic. In Proceedings 15th International Conference on Quantum Physics and Logic, QPL 2018, Halifax, Canada, 3-7th June 2018, 85--105. doi: 10.4204/EPTCS.287.5 Duncan, 2020Ross Duncan, Aleks Kissinger, Simon Perdrix and John van de Wetering. 2020. Graph-theoretic Simplification of Quantum Circuits with the ZX-calculus. Quantum 4 (June 2020, 279). doi: 10.22331/q-2020-06-04-279.

However, such properties of the transition system – or successful heuristic approximations for it – cannot always be derived. In these cases, the space of graphs reachable from an input graph within the transition system must be explored non-deterministically. In the absence of a control program, GROOVE will fall back to an exhaustive exploration of the search space – for an exploration up to depth $\Delta$, the result is a search tree of size $\mathcal O(\gamma^\Delta)$, where $\gamma$ is the number of possible rewrites at every graph in the search space (assuming $\gamma$ is constant for every reachable graph).

Exhaustive exploration is used extensively in model checking, typically to verify properties that must hold for all reachable graphs Rensink, 2004Arend Rensink, Ákos Schmidt and Dániel Varró. 2004. Model Checking Graph Transformations: A Comparison of Two Approaches. In Graph Transformations. ICGT 2004. Springer Berlin Heidelberg, 226--241. doi: 10.1007/978-3-540-30203-2_17. It has also proven to be very useful for compiler optimisation, where the constantly evolving rewrite rules, instruction sets and complex, architecture-dependent cost functions render it challenging to fix a deterministic program transformation schedule.

Jia et al. showed in Jia, 2019Zhihao Jia, Oded Padon, James Thomas, Todd Warszawski, Matei Zaharia and Alex Aiken. 2019. TASO: optimizing deep learning computation with automatic generation of graph substitutions. In Proceedings of the 27th ACM Symposium on Operating Systems Principles, October 2019. ACM, 47--62. doi: 10.1145/3341301.3359630 that computation graph optimisation using graph transformations was achievable without predefined rewriting strategies. They discovered new state-of-the-art implementations for computation graphs of interest to the deep learning community using a simple exhaustive search of the space of possible rewrites with backtracking. This approach was then adapted to quantum circuit optimisation 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.

These recent results fit within a long line of compiler research called superoptimisation Fraser, 1979Christopher W. Fraser. 1979. A compact, machine-independent peephole optimizer. In Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL ’79. ACM Press, 1--6. doi: 10.1145/567752.567753 Massal., 1987Henry Massalin. 1987. Superoptimizer: a look at the smallest program. In Proceedings of the second international conference on Architectual support for programming languages and operating systems, October 1987. ACM, 122--126. doi: 10.1145/36206.36194 Sands, 2011Duncan Sands. 2011. Super-optimizing LLVM IR. (November 2011). Retrieved on 13/01/2025 (LLVM Developer's meeting) from http://llvm.org/devmtg/2011-11/Sands_Super-optimizingLLVMIR.pdf Bansal, 2006Sorav Bansal and Alex Aiken. 2006. Automatic generation of peephole superoptimizers. ACM SIGARCH Computer Architecture News 34, 5 (October 2006, 394--403). doi: 10.1145/1168919.1168906 Sasnau., 2017Raimondas Sasnauskas, Yang Chen, Peter Collingbourne, Jeroen Ketema, Jubi Taneja and John Regehr. 2017. Souper: A Synthesizing Superoptimizer. CoRR abs/1711.04422. On top of excellent optimisation performance, this approach to compiler optimisation using graph transformation systems (GTS) is exceptionally flexible, as rewrite rules can be generated and tailored on demand to the constraints and instruction set of the target hardware. For any supplied cost function, the compiler can explore all valid program transformations to find the rewrites sequence that minimises cost. This keeps the cost function-specific logic separate from the transformation semantics of the program, making it straightforward to replace or update the optimisation objective.

The adaptation of superoptimisation to quantum optimisation of 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 is, however, showing scaling difficulties: unlike classical superoptimisation, which is usually designed to optimise small subroutines within programs, e.g. focusing on arithmetic instructions, single instruction multiple data (SIMD) etc., the technique should in principle be able to optimise quantum programs in their entirety and requires tens of thousands of rewrite rules. This leads to immense search spaces that superoptimisation does not scale well to.

For the special case of term rewriting, i.e. rewriting of tree expressions, a technique known as equality saturation was introduced in Tate, 2009Ross Tate, Michael Stepp, Zachary Tatlock and Sorin Lerner. 2009. Equality saturation: a new approach to optimization. ACM SIGPLAN Notices 44, 1 (January 2009, 264--276). doi: 10.1145/1594834.1480915 to compress and reduce the size of the search space significantly. Equality saturation can be viewed as a twist on persistent data structures designed to optimise terms through term rewriting. It is persistent insofar as it preserves all data inserted into it, though, unlike persistent data structures, it does not retain the history of transformations. This introduces a new step in the optimisation process known as the extraction phase, where the best term stored within the data structure must be identified and recovered.

An efficient implementation was presented in Willsey, 2021Max Willsey. 2021. Practical and Flexible Equality Saturation. PhD Thesis. University of Washington, and it has recently been adopted in modern compiler optimisation pipelines Fallin, 2022Chris Fallin. 2022. Cranelift: Using E-Graphs for Verified, Cooperating Middle-End Optimizations. (August 2022). Retrieved on 14/01/2025 (RFC) from https://github.com/bytecodealliance/rfcs/blob/main/accepted/cranelift-egraph.md. Though the approach was extended to optimise computation graphs for deep learning in Yang, 2021Yichen Yang, Mangpo Phitchaya Phothilimtha, Yisu Remy Wang, Max Willsey, Sudip Roy and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. CoRR abs/2101.01332. doi: 10.48550/ARXIV.2101.01332, equality saturation does not generalise to graph rewriting. Equality saturation and the difficulties of adapting it to graph rewriting are interesting (and subtle!) enough to warrant their own section.

5.2. A closer look at equality saturation

Below, we provide a succinct introduction to equality saturation and discuss its shortcomings in the context of quantum computation and graph rewriting in general. For further details on equality saturation, we recommend the presentation of Willsey, 2021Max Willsey. 2021. Practical and Flexible Equality Saturation. PhD Thesis. University of Washington, its implementation Willsey, 2025Max Willsey. 2025. egg: egraphs good. Retrieved on 14/01/2025 (code repository) from https://github.com/egraphs-good/egg, and this blog discussion Bernst., 2024Max Bernstein. 2024. What's in an e-graph?. (Septempter 2024). Retrieved on 14/01/2025 (blog post) from https://bernsteinbear.com/blog/whats-in-an-egraph/.

Unlike a general-purpose compiler utility, equality saturation is specifically a technique for term rewriting. Terms¹ are algebraic expressions represented as trees, in which tree nodes correspond to operations, the children of an operation are the subterms passed as arguments to the operation, and leaf nodes are either constants or unbound variables. For instance, the term $f(x \times 2, 3)$ would be represented as the tree:

This representation is particularly suited for any pure functional (i.e. side-effect-free) classical computation. Every node of a term is identified with its own term: the subterm given by the subtree the node is the root of. Given term transformation rules, term rewriting consists of finding subterms that match known transformation patterns. The matching subtrees can then be replaced with the new equivalent trees.

In equality saturation, all terms obtained through term rewriting are stored within a single persistent data structure. Term optimisation proceeds in two stages. First, an exploration phase adds progressively more terms to the data structure to discover and capture all possible terms that the input can be rewritten to until saturation (see below), or a timeout, is reached. In the second phase, the saturated data structure is passed to an extraction algorithm tasked with finding the term that minimises the cost function of interest among all terms discovered during exploration.

The data structure that enables this is a generalisation of term trees. Just as in terms, nodes correspond to operations and have children subterms corresponding to the operation’s arguments. To record that a new term obtained through a rewrite is equivalent to an existing subterm, we extend the data structure we employ to also store equivalence classes of nodes, typically implemented as Union-Find data structures Galler, 1964Bernard A. Galler and Michael J. Fisher. 1964. An improved equivalence algorithm. Communications of the ACM 7, 5 (May 1964, 301--303). doi: 10.1145/364099.364331 Cormen, 2009Thomas H Cormen, Charles E Leiserson, Ronald L Rivest and Clifford Stein. 2009. Introduction to algorithms (Third edition ed.). MIT Press, Cambridge, Massachusetts. If we, for instance, applied the rewrite $x * 2 \mapsto x + x$ to the term above, we would obtain

Nodes within a grey box indicate equivalent subterms. This diagram encodes that any occurrence of the x * 2 term can equivalently be expressed by the x + x term. Henceforth, when matching terms for rewriting, both the * term and the + term are valid choices for the first argument of the f operation. Suppose, for example, the existence of a rewrite $f(x + y, z) \mapsto f(x, y * z)$, then this would match the above data structure, resulting in

A consequence of using equivalence relations in the data structure is that the ordering in which the rewrites are considered and applied becomes irrelevant!

As presented, the exploration process would never terminate, and the data structure size would grow indefinitely: as more rewrites are applied, more and more terms are created, resulting in an ever-increasing set of possible rewrites to be considered and processed. Equality saturation resolves this by enforcing a term uniqueness invariant: every term or subterm explored is expressed by exactly one node in the data structure. We can see in the above example that this is currently not the case: the term $x$ for instance, is present multiple times – so is $3$. As a result, the nodes no longer form a forest of trees but instead directed acyclic graphs:

This is commonly known as term sharing, and the resulting data structure is known as a term graph Willsey, 2021Max Willsey. 2021. Practical and Flexible Equality Saturation. PhD Thesis. University of Washington. Maintaining this invariance is not hard in practice: whenever a new term is about to be added by applying a rewrite, it must first be checked whether the term exists already – something that can be done cheaply by keeping track of all hashes of existing terms. In the affirmative case, rather than adding a new term to the matched term’s equivalence class, both terms’ classes must be merged.

It might be that equivalence classes must be merged recursively: given the terms $f(x, 3)$ and $f(y, 3)$, if the classes of $x$ and $y$ are merged (and thus $x$ and $y$ have been proven equivalent), then the classes of their respective parent $f(x, 3)$ and $f(y, 3)$ must also be merged. Doing so efficiently is non-trivial, so we will not go into details here and refer again to Willsey, 2021Max Willsey. 2021. Practical and Flexible Equality Saturation. PhD Thesis. University of Washington.

In the absence of terms of unbounded size, the uniqueness invariant guarantees that the exploration will eventually saturate: as rewrites are applied, there will come a point where all equivalent terms have been discovered, i.e. every applicable rewrite will correspond to an equivalence within an already known class, thereby not providing any new information. This marks the end of the exploration phase².

Term optimisation then proceeds to the extraction phase. Reading out an optimised term out of the saturated term data structure is not trivial. For every equivalence class in the data structure, a representative node must be chosen so that the final term, extracted recursively from the root by always selecting the representative node of every term class, minimises the desired cost function³.

The strategy for choosing representative terms depends heavily on the cost function. In simple cases, such as minimising the total size of the extracted term, this can be done greedily in reverse topological order, i.e. proceeding from the leaves towards the root Willsey, 2021Max Willsey. 2021. Practical and Flexible Equality Saturation. PhD Thesis. University of Washington. There are also more complex cases, however: if the cost function allows for the sharing of subexpressions that may be used more than once in the computation, for instance, then finding the optimal solution will require more expensive computations such as solving boolean satisfiability (SAT) or Satisfiability Modulo Theories (SMT) problem instances Biere, 2021Armin Biere, Marijn J. H. Heule, Hans Maaren and Toby Walsh. 2021. Handbook of satisfiability (Second edition ed.). IOS Press, Amsterdam.

Equality saturation on graphs? #

Equality saturation is a fast-developing subfield of compilation with a growing list of applications. Unfortunately for us⁴, adapting these ideas to quantum computation (and graph rewriting more generally) presents several unsolved challenges.

The root of the problem lies in the program representation. The minIR representation we presented in section 3.3 – but also the quantum circuit representation – captures quantum computations, not as a term, but in a directed acyclic graph (DAG) structure.

A generalisation of equality saturation to computation DAGs was studied in Yang, 2021Yichen Yang, Mangpo Phitchaya Phothilimtha, Yisu Remy Wang, Max Willsey, Sudip Roy and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. CoRR abs/2101.01332. doi: 10.48550/ARXIV.2101.01332 in the context of optimisation of computation graphs for deep learning. Their approach is based on the observation that the computation of a (classical) computation DAG can always be expressed by a term for each output of the computation. Consider, for example, the simple computation that takes two inputs (x, y) representing 2D cartesian coordinates and returns its equivalent in polar coordinates (r, θ).

By introducing two operations $\textit{polar}_r$ and $\textit{polar}_\theta$ that compute $\textit{polar}$ and subsequently, discard one of the two outputs, the DAG can equivalently be formulated as two terms

corresponding to the two outputs r and θ of the computation. This involves temporarily duplicating some of the data and computations in the DAG – though all duplicates will be merged again in the term graph due to the term sharing invariant.

This duplicating and merging of data is fundamentally at odds with the constraints we must enforce on linear data, such as quantum resources. Each operation (or data) of a DAG that is split into multiple terms introduces a new constraint that must be imposed on the extraction algorithm: a computation DAG will only satisfy the no-discarding theorem (section 2.1) for linear values if, for each split operation it contains, it either contains all or none of its split components.

To illustrate this point, consider the following simple rewrite on quantum circuits that pushes X gates ($\oplus$) from the right of a CX gate to the left:

Both the left and right hand sides would be decomposed into two terms, one for each output qubit. The left terms could be written as

whereas the right terms would be

We introduced the term $X(\cdot)$ for the single-qubit X gate and two terms $CX1(\cdot, \cdot)$ and $CX2(\cdot, \cdot)$ for the terms that produce the first, respectively second, output of the two-qubit CX gate. $1$ and $0$ denote the input qubits of the computation. This would be interpreted as two different rewrites

Unlike classical computations, however, either of these rewrites on their own would be unphysical: there is no implementation of either split operations $CX0$ or $CX1$ on their own. We would thus have to enforce at extraction time that for every application of this pair of rewrite rules, either both or none of the rewrites are applied.

Conversely, satisfying the no-cloning theorem requires verification that during extraction, terms that share a subterm but correspond to distinct graph rewrites are never selected simultaneously – otherwise, the linear value corresponding to the shared subterm would require cloning to be used twice.

The no-discarding and no-cloning restrictions result in a complex web of AND respectively XOR relationships between individual terms in the term graph. These constraints could be ignored during the exploration phase and then be modelled in the extraction phase by an integer linear programming (ILP) problem. However, Yang, 2021Yichen Yang, Mangpo Phitchaya Phothilimtha, Yisu Remy Wang, Max Willsey, Sudip Roy and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. CoRR abs/2101.01332. doi: 10.48550/ARXIV.2101.01332 observed that this approach causes the term graph to encode a solution space that grows super-exponentially with rewrite depth (see Fig. 7 in Yang, 2021Yichen Yang, Mangpo Phitchaya Phothilimtha, Yisu Remy Wang, Max Willsey, Sudip Roy and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. CoRR abs/2101.01332. doi: 10.48550/ARXIV.2101.01332), rendering the ILP extraction problem computationally intractable beyond 3 subsequent rewrites. Recent work has attempted to tackle this issue using reinforcement learning Bărbu., 2024George-Octavian Bărbulescu, Taiyi Wang, Zak Singh and Eiko Yoneki. 2024. Learned Graph Rewriting with Equality Saturation: A New Paradigm in Relational Query Rewrite and Beyond. arXiv: 2407.12794 [cs.DB].

Linearity-preserving rewrites are an exponentially small subset #

A simple calculation shows that in the case that all values in the computation graph are linear and only graphs up to a maximal size are considered, the number of possible rewrites only grows exponentially in the rewrite depth. In other words, for optimisation of quantum computations, the solution space of valid computations is much smaller⁵ than the space explored by the equality saturation approach of Yang, 2021Yichen Yang, Mangpo Phitchaya Phothilimtha, Yisu Remy Wang, Max Willsey, Sudip Roy and Jacques Pienaar. 2021. Equality Saturation for Tensor Graph Superoptimization. CoRR abs/2101.01332. doi: 10.48550/ARXIV.2101.01332.

Indeed suppose there is a maximal graph size $|V(G)| \leqslant \Theta$ and suppose that all rewrite patterns, i.e. the subgraph induced by the vertex deletion set $V^-$ of a rewrite, are connected. This is an assumption that was also made in chapter 4, see section 4.2 for a discussion.

In a computation graph of linear values $G$, every vertex (value in the computation) $v \in V(G)$ has a unique incoming and outgoing edge. This means that any pattern embedding $\varphi: P \hookrightarrow G$ is uniquely defined by the image $\varphi(v_P)$ of a single vertex $v_P \in V(P)$. Thus for a GTS with $m$ transformation rules, there can be at most a constant number

of possible rewrites that can be applied to any graph $G$. Let $\mathcal{G}_d$ be the set of all graphs that can be reached in the GTS in at most $d$ rewrites from some input graph $G_0$. $\mathcal{G}_{d+1}$ is the set of all graphs obtained by applying a rewrite to a graph $G \in \mathcal{G}_d$. Thus we have the relation:

The total number of rewrites $R_d$ that can be applied on any graph in $\mathcal{G}_d$ is thus

In summary, equality saturation is a specialisation of persistent data structures uniquely suited to the problem of term rewriting. It succinctly encodes the space of all equivalent terms, and using term sharing does away with the need to apply equivalent rewrites on multiple copies of the same term, which inevitably occurs on more naive rewriting approaches.

However, equality saturation cannot model rewrites that require deleting parts of the data. This is not a problem for terms representing classical operations, as data can always be implicitly copied during exploration and discarded during extraction as required. This is not the case for quantum computations – and for graph rewriting in general, where explicit vertex (and edge) deletions are an integral part of graph transformation semantics.

As a result, numerous constraints would have to be imposed to restrict the solution space encoded by term graphs to valid outcomes of graph rewriting procedures. This would make extraction algorithms complex and cumbersome. More importantly, we showed that in the case of computation graphs on linear values, such as quantum computations, the solution space explored by equality saturation is super-exponentially larger than the space of valid computations, rendering the extraction algorithm and meaningful exploration of the relevant rewriting space computationally intractable.

5.3. The data structure

We now present a data structure that is closely related to equality saturation but supports arbitrary graph rewriting. It is modelled on the graph unfolding construction as presented in Baldan, 2008Paolo Baldan, Andrea Corradini and Barbara König. 2008. Unfolding Graph Transformation Systems: Theory and Applications to Verification.

Rather than maintaining equivalence relations between terms, as done in term graphs, we maintain equivalence relations between graph vertices. Our data structure stores the set of all applied rewrites – the main subject of this section is to show how all operations of interest on this data structure can be implemented efficiently.

The persistent graph rewriting data structure is given by a set $\mathcal{D}$ of events $\delta = (G_R, V^-, \mu) \in \mathcal{D}$, with

• vertex deletion set $V^- \subseteq V(\mathcal{D} \smallsetminus \delta)$ and
• glueing relation $\mu: V^- \rightharpoonup V(G_R)$.

We have extended the $V(\cdot)$ notation to $\mathcal{D}$ by defining it as the union of all vertex sets of replacement graphs in $\mathcal{D}$. We will similarly use $V(\delta)$ to denote the set of vertices in the replacement graph of a rewrite $\delta$.

Events resemble rewrites as defined in Definition . but differ in that they do not apply to a single graph $G$, i.e. there is no graph such that $V^- \subseteq V(G)$. Instead,

We will see below how a graph $G$ can be constructed such that an event $\delta \in \mathcal{D}$ is indeed a valid rewrite on $G$.

Using the disjointness of the union in (1), for all $v \in V(\mathcal{D})$, there is a unique $\delta \in \mathcal{D}$ such that $v \in V(\delta)$ that we call the owner of $v$. The parents (or directed causes) $P(\delta)$ of an event $\delta$ are then the owners of the vertices in the deletion set $V^-$ of $\delta$:

Inversely, we define the children of $\delta$ as the set of event whose parents include $\delta$

The following figure shows an example of a data structure $\mathcal{D}$ on undirected graphs.

Merges, confluent persistence and event creation #

A rewrite $r = (G_R, V^-, \mu)$ that applies to a replacement graph of an event $\delta_p$, i.e. $V^- \subseteq V(\delta_p)$ immediately defines a valid event $\delta_r := r$. In that case, $\delta_r$ has a unique parent

Creating an event $\delta_r$ from a rewrite $r$ is the simplest type of data mutation that can be recorded in $\mathcal{D}$. For $\mathcal{D}$ to be a confluently persistent data structure, it must also be allowed to merge mulitple data mutations together. Rather than handling merges of versions of the data structure explicitly, an event $\delta \in \mathcal{D}$ can define graph mutation operations that apply on collections of events $P \subseteq \mathcal{D}$ – the resulting mutation is equivalent to explicitly creating a merged version of the versions in $P$, followed by the desired rewrite. In this case, the parents of $\delta$ are precisely the set $P = P(\delta)$.

In other words, the parent-child relationships of $\mathcal{D}$ is precisely the event history of $\mathcal{D}$: a directed graph with vertex set $\mathcal{D}$ and edges $\delta_1 \to \delta_2$ if $\delta_1 \in P(\delta_2)$. For $\mathcal{D}$ to define a valid confluently persistent data structure, we need to

1. Ensure that the event history is acyclic, and
2. Define conditions that guarantee that events correspond to valid data mutations.

We hit both birds with one stone by restricting how $\mathcal{D}$ can be constructed and modified in such a way that acyclicity is guaranteed. Specifically, we introduce two procedures:

• CreateEmpty constructs an empty $\mathcal{D} = \varnothing$, and
• AddEvent, adds an event $\delta$ to $\mathcal{D}$.

The first is straightforward – and importantly, the only way to construct an instance $\mathcal{D}$. AddEvent, on the other hand, enforces two conditions that $\delta$ must satisfy to be added to a set $\mathcal{D}$:

• $P(\delta) \subseteq \mathcal{D}$, and
• all parents of $\delta$ must be compatible.

We defer the discussion on the second condition, enforced by the AreCompatible procedure, to its dedicated section below. The restriction $P(\delta) \subseteq \mathcal{D}$ defines a partial order on events by guaranteeing that an event $\delta$ can only be defined and added to $\mathcal{D}$ after all its parents $P(\delta)$ have been added.

We say that $\mathcal{D}$ is valid if it can be constructed from a single call to CreateEmpty, followed by a sequence of calls to AddEvent. This is equivalent to requiring that

1. the parent-child relationship is acylic and
2. the parents of every event satisfy AreCompatible.

For the remainder of this chapter, we will always assume that $\mathcal{D}$ is valid, and thus the event history of $\mathcal{D}$ is always well-defined and acyclic.

def CreateEmpty() -> Set[Event]:
    return set()

def AddEvent(
    events: Set[Event],
    replacement_graph: Graph
    deletion_set: Set[V],
    glueing_relation: EquivalenceRelation[V]
) -> Set[Event]:
    new_event = (
        replacement_graph,
        deletion_set,
        glueing_relation
    )
    parents = parents(new_event)
    assert(issubset(parents, events))
    assert(AreCompatible(parents))

    events = union(events, {new_event})

Compatible events #

Assuming the parent-child relationship is acylic, we can define the ancestors (or causes) $\lfloor\delta\rfloor$ of an event $\delta$ recursively

Events $D \subseteq \mathcal{D}$ are compatible (or a configuration) if all vertex deletion sets $V^-$ for all ancestors of $\delta \in D$ are disjoint. That is, writing

we require that all sets $\{V^- \mid (G_R, V^-, \mu) \in \lfloor D \rfloor \}$ are disjoint. In the example above, events $\delta_5$ and $\delta_6$ are compatible, wheresa $\delta_5$ and $\delta_4$ are not. As pseudocode, this is implemented by the following procedure.

def AreCompatible(events: Set[Event]) -> bool:
    all_ancestors = union([ancestors(d) for d in events])
    deleted_vertices = set()
    for d in all_ancestors:
        for v in deletion_set(d):
            if v in deleted_vertices:
                return False
            deleted_vertices.add(v)
    return True

Note that this definition of event compatibility is a strictly stronger version of parallel independence as is typically defined in DPO rewriting Corrad., 2018Andrea Corradini, Dominique Duval, Michael Löwe, Leila Ribeiro, Rodrigo Machado, Andrei Costa, Guilherme Grochau Azzi, Jonas Santos Bezerra and Leonardo Marques Rodrigues. 2018. On the Essence of Parallel Independence for the Double-Pushout and Sesqui-Pushout Approaches. In Graph Transformation, Specifications, and Nets, Cham. Springer International Publishing, 1--18. doi: 10.1007/978-3-319-75396-6_1. It does not allow for events $\delta_1$ and $\delta_2$ such that a vertex $v$ is both

• in the read only context of $\delta_1$, i.e. $v \in V_1^- \cap dom(\mu_1)$, and thus present both before and after the application of $\delta_1$,
• in the deletion set of $\delta_2$, i.e. $v \in V^-_2$.

This excludes asymmetric conflicts as discussed in e.g. Baldan, 2008Paolo Baldan, Andrea Corradini and Barbara König. 2008. Unfolding Graph Transformation Systems: Theory and Applications to Verification, which arise in the more generali definition. This restriction simplifies our considerations as makes the event history of any event unique.

The runtime is $O(D_A \log D_A)$, where $D_A$ is the sum of the sizes of all vertex deletion sets of events in $\lfloor D \rfloor$

The $\log$ factor can typically be removed if the vertices $v$ span a contiguous integer range or by using a hash function. Alternatively, the $\log$ factor can also be reduced by using separate sets to track deleted vertices of each event.

When talking about compatible sets of events $D \subseteq \mathcal{D}$, it simplifies considerations to always choose $D$ such that the ancestors of $\delta \in D$ are also in $D$, i.e. $D = \lfloor D \rfloor.$ We introduce the notation

for the set of all compatible sets of rewrites of the form $\lfloor D \rfloor$.

Events are rewrites on the flattened history #

We have so far explored how events can be added to $\mathcal{D}$, as well as when they are compatible. However, until we have established that adding events to $\mathcal{D}$ is in some sense equivalent to applying rewrites on a graph, it is hard to see how the data structure $\mathcal{D}$ would be useable for graph rewriting. This is precisely our next point.

In a valid non-empty $\mathcal{D}$, events $\delta \in \mathcal{D}$ form a directed acyclic graph and therefore there must always be (at least) one “root” event $\delta_1 \in \mathcal{D}$ with no parents $P(\delta_1) = \varnothing$. $\delta_1$ is thus a valid rewrite that can be applied to any graph.

For the applications of $\mathcal{D}$ that we consider, it will always be sufficient to have a unique root event $\delta_1$. Viewing $\delta_1$ as a rewrite that applies to the empty graph $G_0 = \varnothing \to G_1$, we can understand it as injecting the input graph $G_1$ into $\mathcal{D}$.

Non-root events in $\mathcal{D}$ on the other hand typically correspond to valid (semantics preserving) rewrites in the GTS under consideration.

Consider a set of compatible events $D \in \Gamma(\mathcal{D})$. Define a topological ordering $\delta_1, \ldots, \delta_k$ of the events in $D$, i.e. if $\delta_j \in P(\delta_i)$ then $i < j$.

This construction is illustrated in the following figure for the compatible set $\lfloor \delta_5 \rfloor \cup \lfloor \delta_6 \rfloor$ of the previous example.

We now show that the graph $G_k$ is determined uniquely by $D \in \Gamma(\mathcal{D})$ and provide an explicit procedure to construct it.

Let us start with the definition of FlattenHistory:

 1def FlattenHistory(events: Set[Event]) -> Graph:
 2    all_ancestors = union([ancestors(d) for d in events])
 3    graph = Graph()
 4    for a in toposort(all_ancestors):
 5        add_graph(graph, replacement_graph(a))
 6        for (del_v, repl_v) in glueing_relation(a):
 7            move_edges(graph, repl_v, del_v)
 8        for v in deletion_set(a):
 9            remove_vertex(graph, v)
10    return graph

toposort is a function that returns a topological ordering of the rewrites in $D$ according to the parent-child rewrite relation, add_graph inserts the graph passed as second argument into the graph passed as first argument, remove_vertex removes the vertex along with all incident edges from the graph and move_edges moves all edges of the second vertex to the first vertex.

Now instead of exploring the space of all graphs $\mathcal{G}$ reachable by repeatedly applying rewrites, we can explore the rewrite space by adding events to $\mathcal{D}$. Write $flat(D)$ for the graph returned by FlattenHistory on set $D$. If $\mathcal{G}'$ is the set of all graphs returned by FlattenHistory on compatible events

then Proposition . and Proposition . combined guarantee that $\mathcal{G}' \subseteq \mathcal{G}$. To conclude, we show that indeed any graph in $\mathcal{G}$ is in $\mathcal{G}'$, and hence $\mathcal{G} = \mathcal{G}'$.

Starting from the empty graph $\mathcal{D} = \varnothing$, we can create a root event $\delta_0 = (G, \varnothing, \varnothing)$ with an empty vertex deletion set and glueing relation and add it to $\mathcal{D}.$

Clearly, $flat(\{\delta_0\}) =G$. We then apply Proposition . repeatedly. If we have a sequence $r_1, \ldots, r_k$ of valid rewrites that can be applied on $G$, then the sequence of events $\delta_1 = r_1, \ldots, \delta_k = r_k$ that it defines can also be added to $\mathcal{D}$ in this order. As we have further seen in Proposition . and Proposition ., the graph $G_k$ that is obtained as a result of the rewrites is the same graph returned by FlattenHistory called on $D = \mathcal{D}$.

In other words, we conclude that exploring the rewrite space on $G$ is fully equivalent to exploring the space of valid events starting from $\mathcal{D} = \{ \delta_0 \}$.

5.4. Exploration and extraction

In the previous section, we proposed a data structure $\mathcal{D}$ that is confluently persistent and can be used to explore the space of all possible transformations of a graph transformation system (GTS). We are now interested in using $\mathcal{D}$ to solve optimisation problems over the space of reachable graphs in the GTS. Following the blueprint of equality saturation (see section 5.2), we proceed in two phases:

1. Exploration.  Given an input graph $G$, populate $\mathcal{D}$ with events that correspond to rewrites applicable to graphs reachable from $G$,
2. Extraction.  Given a cost function $f$, extract the optimal graph in $\mathcal{D}$, i.e. the graph that is a flattening of a set of compatible edits $D \subseteq \mathcal{D}$ and minimises $f$.

Each phase comes with its respective challenges, which we discuss in this section. We will first look at the exploration phase, which requires a way to find and construct new events $\delta$ that can be added to $\mathcal{D}$. We will consider the extraction phase in the second part of this section and see that the problem of optimisation over the power set $\mathcal P(\mathcal D)$ can be reduced to boolean satisfiability formula that admit simple cost functions in the use cases of interest.

There is an additional open question that we do not cover in this section and would merit a study of its own: the choice of heuristics that guide the exploration phase to ensure the “most interesting parts” of the GTS rewrite space are explored. We propose a very simple heuristic to this end in the benchmarks of section 5.5, but further investigations are called for.

Exploring the data structure with pattern matching #

We established in the previous section that rewrites that apply on $G$ can equivalently be added as events to $\mathcal{D}$. In other words, a graph $G'$ is reachable from $G$ using the rewrites of a GTS if and only if there is a set of compatible events $D \subseteq \mathcal{D}$ such that $G'$ is the graph obtained from FlattenHistory on input $D$.

To expand $\mathcal{D}$ to a larger set $\mathcal{D}' \supseteq \mathcal{D}$, we must find all applicable rewrites on all graphs within $\mathcal{D}$. A naive solution would iterate over all subsets of $D \subseteq \mathcal{D}$, check whether they form a compatible set of events, compute FlattenHistory if they do, and finally run pattern matching on the obtained graph to find the applicable rewrites. We can do better.

The idea is to traverse the set of events in $\mathcal{D}$ using the glueing relations $\mu$ that connect vertices between events. Define the function $\bar{\mu}: V(\mathcal{D}) \to \mathcal{P}(V(\mathcal{D}))$ that is the union of all glueing relations $\mu$ in events in $\mathcal{D}$:

where we write $\delta_v$ for the owner of $v$, i.e. the (unique) event $\delta_v \in \mathcal{D}$ such that $v \in V(\delta_v)$. We define the set $\mathcal{E}_D(v)$ of equivalent vertices of $v$ that are compatible with $D$ by applying $\bar\mu(v)$ recursively and filtering out vertices whose owner is not compatible with $D$. It is easiest to formalise this definition using pseudocode for the EquivalentVertices procedure. The set of vertices in $\mathcal{E}_D(v)$ are vertices of descendant events of $\delta_v$.

def EquivalentVertices(
    v: Vertex, events: Set[Event]
) -> Set[Vertex]:
    all_vertices = set({v})
    for w in mu_bar(v):
        new_events = union(events, {owner(w)})
        if AreCompatible(new_events):
            all_vertices = union(all_vertices,
                EquivalentVertices(w, new_events)
            )
    return all_vertices

Whilst it looks as though EquivalentVertices does not depend on $\mathcal{D}$, it does so through the use of the function calls to mu_bar.

We use EquivalentVertices to repeatedly extend a set of pinned vertices $\pi \subseteq V(\mathcal{D})$. A set of pinned vertices must satisfy two properties:

• the set $D_\pi = \{\delta_v \mid v \in \pi \}$ is a set of compatible events,
• there is no vertex $v \in \pi$ and event $\delta \in D$ such that $v \in V^-(\delta)$.

As a result, for the flattened graph $G = flat(D_\pi)$, it always holds that $\pi \subseteq V(G)$. Furthermore, if $G(\pi) \subseteq G$ is the subgraph of $G$ induced by $\pi$, then for any superset of pinned vertices $\pi' \supseteq \pi$, we have $G(\pi) \subseteq G'(\pi')$ where $G' = flat(D_{\pi'})$. In other words: extending a set of pinned vertices results in an extension of the flattened graph – a very useful property when pattern matching. This property follows from the second property above and the definition of FlattenHistory.

This gives us the following simple procedure for pattern matching:

1. Start with a single pinned vertex $\pi = \{v\}$.
2. Construct partial embeddings $P \rightharpoonup G(\pi)$ for patterns $P$.
3. Pick a new vertex $v$ in $G = flat(D_\pi)$ but not in $G(\pi)$ (that we would like to extend the domain of definition of our pattern embeddings to).
4. For all vertices $v' \in \mathcal{E}_D(v)$, build new pinned vertex sets $\pi' = \pi \cup \{v'\}$, filter out the sets $\pi'$ that are not valid pinned vertex sets.
5. Repeat steps 2–4 until all pattern embeddings have been found.

Step 1 is straightforward – notice that pattern matching must be started at a vertex in $V(\mathcal{D})$, so finding all patterns will require iterating over all choices of $v$. The pattern embeddings are constructed over iterations of step 2: each iteration can be seen as one step of the pattern matcher – for instance, as presented in chapter 4 – extending the pattern embeddings that can be extended and discarding those that cannot. If all possible pattern embeddings have been discarded, then matching can be aborted for that $\pi$ set.

How step 3 should be implemented depends on the types of graphs and patterns that are matched on. It is straightforward in the case of computation graphs with only linear values, i.e. hypergraphs with hyperedges that have directed, ordered endpoints and vertices that are incident to exactly one incoming and one outgoing edge. In that case, $v$ can always be chosen in such a way as to ensure progress on the next iteration of step 2, i.e. the domain of definition of at least one partial pattern embedding $P \hookrightarrow G(\pi)$ will be extended by one vertex. The text in the blue box below explains this case in more detail.

Step 4 produces all possible extensions of $\pi$ to pinned vertex sets $\pi'$ that include a descendant $v'$ of $v$ (or $v$ itself). All vertices in $\mathcal{E}_D(v)$ are in events compatible with $D$ by definition, so to check that $\pi'$ is a valid pinned vertex set, we only need to check the second property of pinned vertices. Let $P$ be a pattern, let $S$ be the set of all $\pi$ sets under consideration. Step 4 increments the sizes of all pinned vertex sets $\pi \in S$ whilst maintaining the following invariant.

Invariant for step 4.  If there is a superset $D' \supseteq D_\pi$ of compatible events such that $P$ embeds in $G' = flat(D')$, then there is a superset $\pi' \supseteq \pi$ of vertices such that $P$ embeds in $flat(D_{\pi'})$.

Finally, step 5 ensures the process is repeated until, for all partial pattern embeddings, either the domain of definition is complete, or the embedding of $P$ is not possible. Given that step 4 increments the size of $\pi$ sets at each iteration, this will terminate as long as the vertex picking strategy of step 3 selects vertices that allow to extend (or refute) the partial pattern embeddings constructed and extended in step 2. This is satisfied, for example, in the case of linear minIR graphs, as explained in the box.

Choosing the next vertex to pin in linear minIR (step 3).   Assuming patterns are connected, for any partial pattern embedding $P \hookrightarrow G(\pi)$ there is an edge $e_P \in E(P)$ with no image in $G(\pi)$ but such that at least one of the endvertex $v_P$ of $e_P$ has an image $v_G$ in $\pi$ – say, $e_P$ is the outgoing edge of $v_P$. Let $v'_P$ be an endvertex of $e_P$ in $P$ that has no image in $G(\pi)$ – and say, it is the $i$-th outgoing endvertex of $e_P$ in $P$.

Then $v_P$ uniquely identifies an edge $e_G$ in $G = flat(D_\pi)$ – the unique outgoing edge of $v_G$ – which, in turn, uniquely identifies a vertex $v'_G \in V(G)$ – the $i$-th outgoing endvertex of $e_G$. By choosing $v'_G$ in step 3, step 4 will create pinned vertex sets that include all possible vertices equivalent to $v_G'$, which are all vertices that $v_G$ might be connected to through its outgoing edge¹. The next iteration of step 2 will then either extend the partial pattern embedding to $v_P$ or conclude that an embedding of $P$ is not possible.

Using the approach just sketched, pattern matching can be performed on the persistent data structure $\mathcal{D}$. The runtime of steps 2 and 3 depend on the type of graphs and patterns that are matched on – these are, however, typical problems that appear in most instances of pattern matching, independently of the data structure $\mathcal{D}$ used here. A concrete approach to pattern matching and results for the graph types of interest to quantum compilation was presented in chapter 4.

The runtime of step 4 and the number of overall iterations of steps 2–4 required for pattern matching will depend on the number of events in $\mathcal{D}$ (AreCompatible runs in runtime linear in the number of ancestors), the number of equivalent vertices that successive rounds of step 4 will return and the types of patterns and pattern matching strategies.

Extraction using SAT #

Moving on to the extraction phase, we are now interested in extracting the optimal graph from $\mathcal{D}$, according to some cost function of interest. Unlike exploring the “naive” search space of all graphs reachable in the GTS, the optimal solution within the persistent data structure $\mathcal{D}$ cannot simply be read out.

We showed in section 5.3 that finding an optimal graph $G'$ that is the result of a sequence of rewrites on an input graph $G$ is equivalent to finding an optimal set of compatible events $D \in \Gamma(\mathcal{D}) \subseteq \mathcal{P}(\mathcal{D})$ – the optimal graph $G'$ is then recoved by taking $G' = flat(D)$.

There are $2^{|\mathcal{D}|}$ elements in $\mathcal{P}(\mathcal{D})$, which we encode as a boolean assignment problem by introducing a boolean variable $x_\delta$ for all events $\delta \in \mathcal{D}$. The set of events $D$ is then given by

We can constrain the boolean assignments to compatible sets $D$ by introducing a boolean formula

for all $\delta,\delta' \in \mathcal{D}$ such that their vertex deletion sets intersect $V^-(\delta) \cap V^-(\delta') \neq \varnothing$. Any assignment of $\{x_\delta \mid \delta \in \mathcal{D}\}$ that satisfies all constraints of this format defines a compatible set of events.

How many such pairs of events $(\delta,\delta'$) are there? By definition of parents, two events $\delta$ and $\delta'$ can only have overlapping vertex deletion sets if they share a parent. Assuming all events have at most $s$ children, ensuring $D$ is a set of compatible events requires at most $O(s^2 \cdot |\mathcal{D}|)$ constraints.

To further restrict to $D \in \Gamma(\mathcal{D})$, i.e. to sets of compatible events $D = \lfloor D \rfloor$ that contain all ancestors, we can add the further constraints: $\delta \in D$ implies $P(\delta) \subseteq D$. This introduces up to $s \cdot |\mathcal{D}|$ implication constraints

for all $\delta,\delta' \in \mathcal{D}$ such that $\delta' \in children(\delta)$.

For any set of events $\mathcal{D}$, the conjunction of all constraints presented above, i.e. the event compatibility constraints (1) and the parent-child relation constraints (2), defines a boolean satisfiability problem (SAT) with variables $x_\delta$. We have shown:

Finding the optimal assignment #

We now have to find the optimal assignment among all satisfiable assignments for the SAT problem given above. In the most general case where the cost function $f$ to be minimised is given as a black box oracle on the graph $G'$, i.e. on the flattened history of the solution set $D \subseteq \mathcal{D}$, this optimisation problem is hard².

However, if $f$ can be expressed as a function of $x_\delta$ instead of the flattened history $G' = flat(D)$, then the ‘hardness’ can be encapsulated within an instance of a SMT problem (satisfiability modulo theories Nieuwe., 2006Robert Nieuwenhuis and Albert Oliveras. 2006. On SAT Modulo Theories and Optimization Problems. In Theory and Applications of Satisfiability Testing - SAT 2006. Springer Berlin Heidelberg, 156--169. doi: 10.1007/11814948_18 Barrett, 2018Clark Barrett and Cesare Tinelli. 2018. Satisfiability Modulo Theories), a well-studied generalisation of SAT problems for which highly optimised solvers exist 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. A class of cost functions for which the SMT encoding of the optimisation problem becomes particularly simple are local cost functions:

The cost $\Delta f_r$ of a rewrite $r$ also immediately defines a cost to the event that $r$ defines $\delta = r$. We can thus associate a cost $\Delta f_\delta$ with each event $\delta \in \mathcal{D}$, given by the cost of any of the rewrites that $\delta$ defines.

An instance of such a local cost function often used in the context of the optimisation of computation graphs are functions of the type

for some vertex weight function $w$ – i.e. cost functions that can be expressed as sums over the costs $w(\cdot)$ associated to individual vertices in $G$³. Indeed, it is easy to see that in this case we can write

where $V^-$ and $V_R$ are the vertex deletion set and replacement graph of $r$ respectively.

As discussed in section 2.2, many of the most widely used cost functions in quantum compilation are local, as the cost of a quantum computation is often estimated by the required number of instances of the most expensive gate type (such as \texttt{CX} gates on noisy devices, or \texttt{T} gates for hardware with built-in fault tolerance protocols).

In these cases, the cost function is integer valued and the extraction problem is indeed often sparse:

In case of $\varepsilon$-sparse local cost functions, the SAT problem on $\mathcal{D}$ can be simplified to only include

by repeatedly applying the following constraint simplification rules on any $\delta_0 \in \mathcal{D}$ such that $\Delta f_{\delta_0} = 0$:

• for every parent $\delta_p \in parents(\delta_0)$ and child $\delta_c \in children(\delta_0)$, remove the parent-child constraints between $\delta_p$ and $\delta_0$ and between $\delta_0$ and $\delta_c$. Insert in their place a parent-child constraint between $\delta_p$ and $\delta_c$.
• for every non-compatible sibling event $\delta_s \in \mathcal{D}, \delta_s \neq \delta_0$, remove the compatibility constraint between $\delta_0$ and $\delta_s$. Insert in its place a compatibility constraint between $\delta_s$ and $\delta_c$ for all $\delta_c \in children(\delta_s)$.

This reduces the SAT or SMT problem to a problem with $|\mathcal D_{\neq 0}| = \varepsilon |\mathcal{D}|$ variables and at most $O(min(|\mathcal{D}|, \varepsilon^2|\mathcal{D}|^2)$ constraints.

With the completion of this section, we have described an equivalent computation on $\mathcal{D}$ for every step of a GTS-based optimisation problem:

1. a rewrite that can be applied on a graph $G$ can be added as an event to $\mathcal{D}$,
2. a graph $G'$ that results from a sequence of rewrites can be recovered from $\mathcal{D}$ using FlattenHistory,
3. the set of all graphs reachable from events in $\mathcal{D}$ can be expressed as a SAT problem; depending on the cost function, the optimisation over that space can then take the form of an SMT problem.

In essence, using the confluently persistent data structure $\mathcal{D}$ we replace a naive, exhaustive search over the space $\mathcal{G}$ of all graphs reachable in the GTS with a SAT (or SMT) problem – solvable using highly optimised dedicated solvers that could in principle handle search spaces with up to millions of possible rewrites Zulkos., 2018Edward Zulkoski. 2018. Understanding and Enhancing CDCL-based SAT Solvers. PhD Thesis. University of Waterloo.

5.5. Bounding the search space size

We show in this section that under some assumptions on the GTSs that hold in the use cases of interest to quantum compilation, there is a provable gap between the size of the search space of all reachable graphs in the GTS and the size of the corresponding confluently persistent data structure $\mathcal{D}$.

Let us introduce first the notion of overwriting rewrites.