+++
title = "Related work"
layout = "section"
weight = 1
slug = "sec:sota_parallel"
+++

The unfolding of a graph transformation system (GTS) was first proposed in
@Baldan1999a as a generalisation of a well-known construction on Petri nets
@Winskel1987. Originally defined for DPO rewriting, the unfolding was later
generalised to SPO @Baldan2007 @Baldan2014 and SqPO @Behr2019 in arbitrary
adhesive categories. The unfolding is a powerful GTS technique that has found
applications in model verification @Baldan2008 @Baldan2008b @Costa2012 and other
formal analysis tools such as model-based diagnosis @Baldan2008a and model
transformation analysis @Bisztray2009.

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 @Baldan2008 @Baldan2004
@Baldan2008c @Baldan2010 @Schwoon2013. On the other hand, unfoldings of GTSs of
quantum computation are expected to be intractably large @Yang2021, 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 @Driscoll1989 @Lagogiannis2005, and particularly within functional
programming @Okasaki1996 @Okasaki1998 @Hinze2005. Confluently persistent data
structures were first explored in @Driscoll1994. A general treatment of the
approach was subsequently presented in @Fiat2003 and improved in @Collette2012.
@Chalermsook2018 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. @Corradini1996 and
Baldan et al. @Baldan1999. This categorical formalism has also been extended to
include support for overlapping transformations in @Echahed2017.

The first practical application of persistent graph rewriting was developed by
the graph rewriting engine GRAPE @Weber2017 and was originally based on
ephemeral data structures with transactional ACID semantics. Later, its
successor, GrapeVine @Weber2022, 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 {{< reflink "sec:factor-gts" >}}, 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
@Echahed2008. This distinguishes the approach presented in this thesis from most
previous work. Rewriting strategies feature prominently in PORGY, a tool for
port graph rewriting @Andrei2011 @Fernandez2010; the graph rewriting software
GROOVE provides the notion of a _control program_ to govern the transformation
order @Rensink2004; and finally, tools such as GrGen provide advanced control
flow primitives to specify rewrite rule execution @Geiss2006.

Specifying rewriting strategies yields efficient graph transformation procedures
and is particularly effective for systems with provable properties such as
confluence and termination @Verma1995. As a result, rewriting strategies have
also been used successfully within classical compiler optimisations @Assmann2000
and quantum circuit optimisation @Fagan2018 @Duncan2020.

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 @Rensink2004a. 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 @Jia2019 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 @Xu2022 and @Xu2023.

These recent results fit within a long line of compiler research called
_superoptimisation_ @Fraser1979 @Massalin1987 @Sands2011 @Bansal2006
@Sasnauskas2017. 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 @Xu2022 and
@Xu2023 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 @Tate2009 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 @Willsey2021, and it has recently
been adopted in modern compiler optimisation pipelines @Fallin2022. Though the
approach was extended to optimise computation graphs for deep learning in
@Yang2021, 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.
