Compositionality and Connectivity: Diagrammatic Reasoning in Proof Assistants

Process theories capture computation as a compositional structure. Similar to circuits, they care about representing processes as blocks which can be compose in sequence or in parallel. This makes them a valuable abstraction when it comes to reasoning about programs, particularly process theories such as the ZX-Calculus have found use in reasoning about quantum programs. The primary benefit of process theories for reasoning is their corresponding diagrammatic calculi. This makes them great for pen and paper reasoning, but leaves a gap in applying this style of reasoning within formal verification. Working on pen and paper avoids a large amount of the reasoning one has to do to convince a proof assistant of correctness. We explore how to implement diagrammatic calculi in the concrete case of the ZX-Calculus and also as an abstract structure. Initially we focus on them as purely compositional structures. This ends up being insufficient to capture the reasoning power of diagrammatic calculi. We can improve our ability to capture this reasoning by working with hypergraphs alongside the categorical structures used to represent process theories. This works for concretely sized diagrams, but is insufficient for parametrically sized diagrams. To accomplish this, we work with sized hypergraphs, which act as concretely defined hypergraphs with vertex labels representing the parametric size of each vertex. With this, we are able to compute directly on the non-parametric hypergraph portion of the sized hypergraph in order to reason diagrammatically within a proof assistant. This allows us to capture full diagrammatic reasoning within a proof assistant, as we can even handle variables, which are commonly written to represent a parametric number of wires.