Graphical languages are powerful and useful to represent, rewrite and simplify different kinds of processes. In particular, they have been widely used for quantum processes, improving the state of the art for compilation, simulation and verification. In this work, we focus on one of the main carrier of quantum information and computation: linear optical circuits. We introduce the LO_fi-calculus, the first graphical language to reason on the infinite-dimensional photonic space with circuits only composed of the four core elements of linear optics: the phase shifter, the beam splitter, and auxiliary sources and detectors with bounded photon number. First, we study the subfragment of circuits composed of phase shifters and beam splitters, for which we provide the first minimal equational theory. Next, we introduce a rewriting procedure on those LO_fi-circuits that converge to normal forms. We prove those forms to be unique, establishing both a novel and unique representation of linear optical processes. Finally, we complement the language with an equational theory that we prove to be complete: two LO_fi-circuits represent the same quantum process if and only if one can be transformed into the other with the rules of the LO_fi-calculus.

We introduce the first complete equational theory for quantum circuits. More precisely, we introduce a set of circuit equations that we prove to be sound and complete: two circuits represent the same unitary map if and only if they can be transformed one into the other using the equations. The proof is based on the properties of multi-controlled gates – that are defined using elementary gates – together with an encoding of quantum circuits into linear optical circuits, which have been proved to have a complete axiomatisation.

We introduce the LO_v-calculus, a graphical language for reasoning about linear optical quantum circuits with so-called vacuum state auxiliary inputs. We present the axiomatics of the language and prove its soundness and completeness: two LO_v-circuits represent the same quantum process if and only if one can be transformed into the other with the rules of the LO_v-calculus. We give a confluent and terminating rewrite system to rewrite any polarisation-preserving LO_v-circuit into a unique triangular normal form, inspired by the universal decomposition of Reck et al. (1994) for linear optical quantum circuits.