{'fraction_non_alphanumeric': 0.05684214714893956, 'fraction_numerical': 0.013907126656320878, 'mean_word_length': 3.74268729949047, 'pattern_counts': {'":': 0, '<': 12, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 39, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
PBS-calculus: A Graphical Language for Quantum-Controlled Computations

We introduce the PBS-calculus to represent and reason on quantum computations involving polarising beam splitters (PBS for short). PBS-diagrams can be used to represent various schemes including quantum-controlled computations, which are known to have multiple computational and communication advantages over classically ordered models like quantum circuits. The PBS-calculus is equipped with an equational theory, which is proved to be sound and complete: two diagrams are representing the same quantum evolution if and only if one can be transformed into the other using the rules of the PBS-calculus. Moreover, we show that the equational theory is minimal. Finally, we show that any PBS-diagram involving only unitary matrices can be transformed into a diagram without feedback loop.


Introduction
Quantum optics is at the heart of quantum technologies. It is prominent in the implementation of quantum protocols (quantum key distribution [22,39,29], quantum teleportation [9,30]). Quantum optics can also be used for the implementation of the quantum computer [33,28] using for instance the so-called KLM model [26] or other linear optical quantum computation models [27,32,10]. Boson sampling [1], while being a non-universal model, is an optics-based candidate for demonstrating a computational quantum advantage over classical computers.
In the recent years, quantum optics also emerges as a key ingredient for the implementation of quantum computations without definite causal structure [12], and more precisely for quantum-controlled ordering of gates [4]. The quantum switch (see Figure 1.b) is the simplest example of such quantum evolution. The order in which two black boxes U and V are applied is controlled by a qubit: when this qubit is in a superposition state, both U • V and V • U are applied, in superposition. The quantum switch cannot be implemented with a single copy of U and a single copy of V in the quantum circuit model, and more generally using any language with a fixed or classically controlled order of operations. Such a quantum control has been proved to enable various computational and communication advantages over classically ordered models [4,17,18,20,2], for instance for deciding whether two unitary transformations are commuting or anti-commuting [11] (see Example 10). Quantum switch has also been realised experimentally [34,35].
The implementation of quantum-controlled operations in quantum optics relies on the peculiar behaviour of the polarising beam splitter. A polarising beam splitter transforms a superposition of polarisations into a superposition of positions: if the polarisation is horizontal the photon is reflected whereas it is transmitted when the polarisation is vertical (see Figure 1.a). As a consequence a photon can be routed in different parts of a scheme, this routing being quantumly controlled by the polarisation of the photon. This is a unique behaviour which has no counterpart in the quantum circuit model for instance.
We introduce the PBS-calculus to represent and reason on quantum optics computations involving polarising beam splitters. The PBS-calculus is a basic graphical language involving beam splitters, polarisation flips, and gates labelled with arbitrary matrices, moreover feedback loops are allowed. In the framework of categorical quantum mechanics, the PBSdiagrams form a Traced PROP.
The behaviour of a quantum optical scheme involving polarising beam splitters is usually computed intuitively by considering how a particle is routed through the scheme when its polarisation is classical. We formalise this behaviour as a big-step semantics, called path semantics. We also introduce a denotational semantics and prove the adequacy of the denotational semantics with respect to the path semantics.
The PBS-calculus is equipped with an equational theory which can be used to simplify, or more generally, to transform diagrams. We show that the PBS-calculus is sound (the equational theory preserves the semantics) and complete (if two diagrams have the same semantics then one can be transformed into the other using the equational theory). We also show that the equational theory, which is made of ten fairly simple equations, is minimal in the sense that each of these ten equations is necessary for the completeness of the language.
As an application of the PBS-calculus, we consider the problem of unrolling the feedback loops of the PBS-diagrams. Indeed, an interesting property of PBS-diagrams, pointed out by the semantics of the language, is that each feedback loop is used a bounded number of times, namely at most 2. It leads to the natural question of unrolling the loops to make the diagrams loop-free. We point out some counter examples of PBS-diagrams which require feedback loops. We prove, however, that all feedback loops can be removed when all the matrices labelling the gates of the diagram are unitary. We also show that the process of removing the loops requires the introduction of matrices which were not originally present in the initial diagram. Related works. In the context of categorical quantum mechanics several graphical languages have already been introduced: ZX-calculus [13,23], , ZH-calculus [5] and their variants. Notice in particular a proposal for representing fermionic (non polarising) beam splitters in the ZW-calculus [15]. An apparent difference between the PBS-calculus and these languages, is that the category of PBS-diagrams is traced but not compact closed. This difference is probably not fundamental, as for any traced monoidal category there is a completion of it to a compact closed category [24]. The fundamental difference is the parallel composition: in the PBS-calculus two parallel wires correspond to two possible positions of a

Syntax
A PBS-diagram is made of polarising beam splitters , polarisation flips ¬ , and gates U for any matrix U ∈ C q×q , where q is a fixed positive integer. One can also use wires like the identity or the swap . Diagrams can be combined by means of sequential composition •, parallel composition ⊗, and trace T r(·). The trace consists in connecting the last output of a diagram to its last input, like a feedback loop. The symbol represents the empty diagram. Any diagram has a type n → n which corresponds to the numbers of input/output wires. The syntax of the language is the following: Definition 1. Given q ∈ N \ {0}, a PBS q -diagram D : n → n is inductively defined as: : 0 → 0 : 1 → 1 ¬ : 1 → 1 : 2 → 2 : 2 → 2 U ∈ C q×q U : 1→1 D 1 : n→n D 2 : n→n D 2 • D 1 : n→n Sequential composition D 2 • D 1 , parallel composition D 1 ⊗ D 2 , and trace T r(D) are respectively depicted as follows: D1 D2 · · · · · · · · · · D1 · · · · · · · · · · · D2 · · · · · · D In the following, the positive integer q will be omitted when it is useless or clear form the context.
Notice that two distinct terms, like ¬ • ( U • ¬ ) and ( ¬ • U ) • ¬ , can lead to the same graphical representation: ¬ U ¬ . To avoid ambiguity, we define diagrams modulo the structural congruence given in Figure 2. Roughly speaking the structural congruence guarantees that (i) two terms leading to the same graphical representation are equivalent, and (ii) a diagram can be deformed at will, e.g.: In the categorical framework of PROP [31,41], PBS-diagrams modulo the structural congruence form a Traced PROP, i.e. they are morphisms of a traced strict symmetric monoidal category whose objects are natural numbers. It is known (Theorem 20 1 of [37]) that two diagrams are equivalent according to the axioms of a traced PROP if and only if they are isomorphic in a graph-theoretical sense, that is, if one can be obtained from the other by moving, stretching and reorganising the wires in any way, while keeping their two ends fixed.

Semantics
In this section, we introduce the semantics of the PBS-diagrams. First, we introduce an operational semantics for PBS-diagrams with a classical control. The operational semantics, called path semantics is based on the graphical intuition of a routed particle. Then we introduce a denotational semantics for the general case, with a quantum control. We show the adequacy between the two semantics, providing a graphical way to compute the denotational semantics of a PBS-diagram. Single particle. In this paper, we only consider the case where a single particle, say a photon, is present in the diagram. The photon is made of a polarisation and an additional data register. The photon has: an initial polarisation, which is an arbitrary superposition of the two possible classical polarisations {→, ↑}; an arbitrary position, which is a superposition of the possible input wires of the diagram; and an input data state, which is a vector ϕ ∈ C q .

Classical control -Path semantics
Classical control. We first consider input photons with a classical polarisation and a classical position. Roughly speaking, the photon is initially located on one of the input wires with a given polarisation in {→, ↑}, and moves through the diagram depending on its polarisation. The action of a PBS-diagram can be informally described as follows using a token made of the current polarisation c of the photon and a matrix U representing the matrix applied so far to the data register: The photon is either reflected or transmitted by a beam splitter, depending on its polarisation: The polarisation of the photon may vary but remains classical as the polarisation flip -the only one which acts on the polarisation -interchanges horizontal and vertical polarisations: V acts on the data register, transforming the state ϕ into V ϕ: The photon can freely move through wires, e.g.: Thus the token follows a path from the input to the output and accumulates a matrix along the path. We formalize this intuitive behaviour as a big-step operational semantics that we call path semantics in this context. A configuration is a triplet (D, c, p), where D : n → n is a PBS-diagram, c ∈ {→, ↑} is the input polarisation of the photon, and p ∈ [n] := {0, . . . , n − 1} its input position: 0 means that the photon is located on the first upper input wire, 1 on the second one and so on. The result is made of the final polarisation c and position p , and of the matrix U representing the overall action of D on the data register.
Example 3. As expected, the path semantics of the quantum switch (see Figure 1. Notice that the path semantics does not need to be defined for the empty diagram . Indeed, for any diagram D : 0 → 0 there is no valid configuration (D, c, p) as p should be one of the input wires of D.
The (T k )-rule is parametrised by an integer k. Intuitively this parameter is the number of times the photon goes through the corresponding trace. We show in the following that roughly speaking, a particle can never go through a given trace more than twice. In other words, the path semantics which assumes k ≤ 2, is well-defined for any valid configuration: Proof. The proof is given in appendix, section B.1.1.
In the previous proposition, uniqueness means that the path semantics is deterministic. It implies, in particular, that two equivalent diagrams according to the equations of Figure 2 have the same path semantics.
Moreover, all PBS-diagrams are invertible in the following sense: Proof. The proof is given in appendix, Section B.1.1.
As a consequence, any diagram D : n → n essentially acts as a permutation on {→, ↑}×[n], if one ignores its action on the data register. We introduce dedicated notations for representing the corresponding permutation, as well as the actions on the data register:  (D, c, p) [D]c,p ===⇒ τ D (c, p).

Quantum control -Denotational semantics
A crucial property of PBS-diagram is to offer the ability to have a quantum control, i.e. a photon whose input state is a superposition of polarisations, positions, or both. To encounter the quantum control, we introduce in this section a denotational semantics which associates with any diagram a map acting on the state space H n := C {→,↑} ⊗ C n ⊗ C q . Using Dirac notations, {|→ , |↑ } (resp. {|x | x ∈ {0 . . . k − 1}}) is an orthonormal basis of C {→,↑} (resp. C k ). Thus {|c, p, x | c ∈ {→, ↑}, p ∈ [n], x ∈ [q]} is an orthonormal basis of H n . Definition 7. The denotational semantics of a PBS-diagram D : n → n is the linear map D : H n → H n inductively defined as follows: where: Notice that while the denotational semantics is defined by means of an infinite sum, this sum is actually made of a finite number of nonzero elements, which guarantees that the semantics is well-defined: Proposition 8. For any diagram D : n → n, D ∈ S n , where S n is the monoid of the linear maps f ∈ H n → H n such that f |c, p, x = |τ (c, p) ⊗ U c,p |x for some permutation τ on {→, ↑} × [n] and matrices U c,p ∈ C q×q .
Proof. The proof is given in appendix, Section B.1.2.
The denotational semantics is adequate with respect to the path semantics: The adequacy theorem implies that two diagrams have the same denotational semantics if and only if they have the same path semantics. As a consequence, it provides a graphical characterisation of the denotational semantics. Indeed, for any diagram D : n → n, D is, by linearity, entirely defined by τ D and {[D] c,p } c∈{→,↑},p∈ [n] . Since τ D and [D] c,p have a nice graphical interpretation as paths from the inputs to the outputs, the adequacy theorem provides a graphical way to compute the denotational semantics of any PBS-diagram.
We assume that U V = (−1) k V U and call the quantum switch with a control qubit in a uniform superposition:

Equational theory -PBS-calculus
The representation of a quantum computation using PBS-diagrams is not unique, in the sense that two different PBS-diagrams may have the same semantics. In this section, we introduce 10 equations on PBS-diagrams (see Figure 3) as the axioms of a language that we call the PBS-calculus. We prove the PBS-calculus is sound (that is, consistent with the semantics), complete (that is, it captures entirely the semantics equivalence) and minimal (that is, all axioms are necessary to have completeness). Completeness is proved by means of a normal form.

Axiomatisation
Definition 11 (PBS-calculus). Two PBS-diagrams D 1 , D 2 are equivalent according to the rules of the PBS-calculus, denoted PBS D 1 = D 2 , if one can transform D 1 into D 2 using the equations given in Figure 3. More precisely, PBS · = · is defined as the smallest congruence 2 which satisfies equations of figures 2 and 3.
Equations (1) and (6) in Figure 3 reflect the monoidal structure of the matrices, with the identity element (Equation (1)) and the associative binary operation (Equation (6)). Equations (2) and (3) mean that both the polarising beam splitter and the polarisation flip commute with a gate. Moreover, the polarising beam splitter is self inverse (Equation (8)). According to Equation (5), a polarising beam splitter conjugated with polarisation flips is nothing but a polarising beam splitter, up to a permutation of the wires. Another interaction between polarising beam splitters and polarisation flips is given in Equation (10): when two beam splitters are connected directly with a wire and the second branch has a polarisation flip, then the two beam splitters can be merged, up to some polarisation flips. In Equation (4), there are essentially two steps: first, the wire with the gate V is a dead code, as no photon can go to the wire, so it can be discarded; the second step consists in merging the two polarising beam splitters. Equation (9) is the only equation acting on three wires: in this particular configuration given by the left hand side of the equation, two polarising beam splitters can be replaced by swaps.
All these equations preserve the semantics of the PBS-diagrams: Proposition 12 (Soundness). For any two diagrams D 1 and D 2 , if PBS D 1 = D 2 then D 1 = D 2 .
Proof. The proof is given in appendix, Section B.2.1.

Normal forms
In this section we introduce a notion of diagrams in normal form which is used in the next sections to prove both the universality and the completeness of the PBS-calculus. They are made of two parts: the first one corresponds to a superposition of linear maps, and the second one corresponds to a permutation of the polarisations and positions, written in a way that is convenient here. is in NF-sup, and for any U, V ∈ C q×q and any N in Definition 14 (NF-perm). NF-perm diagrams are inductively defined as: is in NF-perm, and for any N : n → n and N : n + 1 → n + 1 in NF-perm, · · · · · · · · · N σ j and · · · · · · · · · N σ j · · · σ k are in NF-perm, where denotes either or ¬ , and σ j : → = · · · · · · · · · j 0 0 −1 . Definition 15 (Normal Form). For any diagrams N 1 : n → n in NF-sup and N 2 : n → n in NF-perm, N 2 • N 1 is in normal form.
In the following we show that any diagram is equivalent to a diagram in normal form.  Proof. Notice that using the axioms of PROP, N 2 = g • . . . • g 0 where each g k consists of either E(U, V ), , ¬ , or acting on any one or two consecutive positions, in parallel with the identity on the other positions. We show that every g k can be successively integrated to the normal form (see appendix, Section B.2.2.1).

Completeness
The main application of the normal forms is the proof of completeness: In particular, one can show inductively that the normal form is entirely determined by its semantics by considering the path semantics for a particle located on the last input wire.

Minimality of the set of axioms
In the following we show that each of the ten equations of Figure 3 is necessary for the completeness of the PBS-calculus: Theorem 21 (Minimality). None of Equations (1) to (10) is a consequence of the others.
Proof. The proof is given in appendix, Section B.2.3.
Notice that all equations involving matrices, except Equation (1), are schemes of equations i.e. one equation for each possible matrix (or matrices). In Theorem 21 we show that each of these equations, for most of the matrices, cannot be derived from the other axioms. More precisely, Equation (4) (resp. (7)) is necessary for completeness for any U (resp. any U, V ); Equation (2) (resp. (6) ) is necessary for completeness for any U = I (resp. any U, V = I). Finally, if det(U ) = 1, then Equation (3) is not a consequence of the others. We conjecture that the condition det(U ) = 1 can be relaxed to U = I.

Universality
A PBS-diagram represents a superposition of linear maps together with a permutation of polarisations and positions. Indeed, Proposition 8 shows that for any diagram D : n → n, D ∈ S n , where S n is the monoid of the linear maps f ∈ H n → H n such that f |c, p, x = |τ (c, p) ⊗ U c,p |x for some permutation τ on {→, ↑} × [n] and matrices U c,p ∈ C q×q .
We show in the following that the PBS-calculus is universal, in the sense that any linear map in S n can be represented by a PBS-diagram.
Theorem 22. The PBS-calculus is universal: for any f ∈ S n , ∃D : n → n, D = f .

Proof.
The proof relies on the normal forms: given a linear map f ∈ S n one can inductively construct a diagram in normal form, by considering the image of f when the photon is located on the last position (p = n − 1).
Notice that S n is strictly included in the set of linear maps from H n to H n . Thus while being universal for S n the PBS-diagrams are not expressive enough to represent a (non polarising) beam splitter for instance.

Removing the trace -Loop unrolling
We consider in this section an application of the PBS-calculus. The semantics of the language points out that each trace, or feedback loop, is used at most twice. As a consequence, a natural question is to decide whether all loops can be unrolled, in order to transform any PBS-diagram into a trace-free PBS-diagram. Such a transformation is possible when all matrices are unitary: Proof. The proof is given in appendix, Section B.3.1.
Notice that Proposition 23 is not true for PBS-diagrams with a single input/output. Indeed a trace-free diagram of type 1 → 1 is made of generators acting on 1 wire only, so in particular it has no polarising beam splitter and as a consequence cannot have a behaviour which depends on the polarisation. For instance, the diagram E(U, V ) used in the normal forms (Definition 13) cannot be transformed into a trace-free diagram unless U = V .
Remark 24. The proof of Proposition 23 actually only needs that the matrices are invertible and have a square root, which is also true for strictly positive Hermitian matrices. Moreover, by polar decomposition and Equation (15), the conclusion of Proposition 23 is still true if we only assume that the matrices are invertible.
On the other hand, PBS-diagrams involving at least one non-invertible matrix are not necessarily equivalent to a trace-free one. Indeed, we have the following property: This prevents the following diagram from being equivalent to a trace-free one: is not equivalent, according to the rules of the PBS-calculus, to any trace-free diagram. Indeed, for any (c, p) Another interesting property is that loop unrolling, when it is possible, requires the use of matrices that were not present in the original diagram. This is a consequence of the following lemma: Lemma 27. Given any diagram D : n → n, let us define |D| := c∈{→,↑},p∈ [n] det ([D] c,p ).

Then for any trace-free diagram D, we have |D|
Proof. Intuitively, due to the invertibility of the PBS-diagrams (Proposition 5), for each wire of a trace-free diagram D, there are exactly two initial configurations which are going through this particular wire. As a consequence each gate of D contributes twice to |D| (see appendix, Section B.3.3).
Example 28. Unless det(U ) is a kth root of unity for some odd integer k, the following diagram D U does not have the same semantics as any trace-free diagram in which all gates are labelled by U :

Conclusion and Perspectives
In this paper, we have introduced a rigorous framework to reason on computations which are sometimes informally represented by schemes involving polarising beam splitters and black boxes. The main result is the introduction of an equational theory which makes the PBS-calculus sound and complete. We have also proved that the axiomatisation is minimal in the sense that each axiom is necessary for the completeness. We believe that the PBS-calculus will be a useful tool to study the power and the limits of computations and protocols involving polarising beam splitters, in particular in the exciting domain of quantum-controlled ordering of gates. We have demonstrated for instance that the PBS-calculus can be used for loop unrolling.
We mention here two perspectives in the development of the PBS-calculus. First, the expressivity of the language can be increased by adding, for instance, a (not polarising) beam splitter as a generator of the language. The presence of such a beam splitter is necessary for the representation of Boson sampling for instance.
Another perspective is to make the calculus more resource-sensitive, by allowing only the equations for which the number of occurrences of each gate (or black box) is preserved. For instance, we have seen examples in which loop unrolling requires to introduce new gates that were not present in the initial diagram. Transforming a diagram into its normal form is another example that does not, in general, preserve the number of occurrences of each gate.

A Categorical notions
Definition 29. A traced PROP is a category C whose objects are the natural integers, equipped with a functor ⊗ : C × C → C such that for any n, m ≥ 0, n ⊗ m = n + m an arrow σ : 2 → 2 a family of functions T r : C(n + 1, m + 1) → C(n, m) satisfying the properties listed below.
Let σ 1,0 := id 1 ; and for any n ≥ 0, let σ 1,n+1 : That C is a category means that it satisfies the following properties: Neutrality of the identity: for any n, m and f : n → m, That ⊗ is a functor means that it satisfies the following properties: Preservation of source and target: for any n, m, k, l ≥ 0, f : n → m and g : k → l, f g Preservation of the identity: for any n, m ≥ 0, = Preservation of composition: for any n, m, m , k, l, l ≥ 0, f 1 : n → m, f 2 : m → m , g 1 : k → l and g 2 : l → l , The additional required properties are: Strict monoidal structure: Naturality of the associator: for any n, n , m, m , k, k , f : n → n , g : m → m and h : k → k , Naturality of the left unitor: for any n, m ≥ 0 and f : n → m, Naturality of the right unitor: for any n, m ≥ 0 and f : n → m, Strict symmetric monoidal structure: Naturality of the swap: for any n, m ≥ 0 and f : n → m, Inverse law: = Axioms about the trace: Naturality in the input: for any n, m, l ≥ 0, f : l → n and g : n + 1 → m + 1, Naturality in the output: for any n, m, l ≥ 0, f : n + 1 → m + 1 and g : m → l, Dinaturality: for any n, m, i, j ≥ 0, f : n + i → m + j and g : j → i, Superposing: for any n, m, l, p ≥ 0, f : n + 1 → m + 1 and g : l → p, Yanking: T r(σ) = id 1 .

=
Remark 30. We can define σ 0,m := id m and for any n ≥ 0, σ n+1,m := (σ n,m ⊗ id 1 ) • (id m ⊗ σ 1,m ). Then the unit coherence σ n,0 = id n and the associativity coherence (id m ⊗ σ n,k ) • (σ n,m ⊗ id k ) = σ n,m+k of the multiwire swaps are consequences of the definition of σ n,m . The general inverse law axiom σ n,m • σ m,n = id n+m can be deduced easily from its restricted version by induction on n and m. The general naturality of the swap, σ n ,m • (f ⊗ g) = (g ⊗ f ) • σ n,m for any f : n → n and g : m → m , can be deduced from its restricted version by first iterating it to get a swap with multiple wires on both sides, then using the general inverse law axiom to flip it upside down. The vanishing axioms T r 0 (f ) = f and T r i (T r j (f )) = T r i+j (f ) are consequences of the definition of T r j . The general yanking axiom T r n (σ n,n ) = id n can be deduced by induction on n from its restricted version using a multiwire version of the Yang-Baxter equation (which is a consequence of the naturality of the swap) and the inverse law. The general (that is, with multiwire traces) versions of naturality of the trace in the input, in the output, and of superposing can be deduced by iteration of their respective restricted versions.
Definition 31. A traced weak braided category is a strict monoidal category that is additionally a weak braided monoidal category in the sense of [19] or [38] and a right traced category in the sense of [37]. A PROTWEB is a traced weak braided category whose objects are generated from the monoidal unit and a single object by monoidal product, and identified with the natural integers.
Namely, a PROTWEB is a category C whose objects are the natural integers, equipped with a functor ⊗ : C × C → C such that for any n, m ≥ 0, n ⊗ m = n + m an arrow σ : 2 → 2 a family of functions T r : C(n + 1, m + 1) → C(n, m) satisfying the properties listed below.
On top of the fact that C is a category and that ⊗ is a functor and acts as the addition on objects, the required properties are, using the same names as in Definition 29: Strict monoidal structure: Naturality of the associator Naturality of the left unitor Naturality of the right unitor Strict weak braided monoidal structure: General naturality of the swap: for any n, n , m, m ≥ 0, f : n → n and g : m → m , Remark 32. Similarly as in the case of the axioms of a traced PROP, the unit coherence and the two associativity coherences (id m ⊗ σ nk ) • (σ nm ⊗ id k ) = σ n(m+k) and (σ nk ⊗ id m ) • (id n ⊗ σ mk ) = σ n(m+k) (which are both needed when σ is not self-inverse) of the multiwire swaps are consequences of the definition of σ nm , the vanishing axioms are consequences of the definition of T r j , and the general versions of naturality of the trace in the input, in the output, and of superposing can be deduced by iteration of their respective restricted versions.

= =
Proof. This follows directly from comparing the lists of axioms given respectively in Definitions 29 and 31, and from the fact that the general naturality of the swap is a consequence of the axioms of traced PROP.

B.1.1 Proof of Propositions 4 and 5
We first prove the two propositions without assuming the axioms of traced PROP. At the end we will have to prove that any two diagrams equivalent modulo the axioms of traced PROP have the same path semantics. Not assuming the axioms of traced PROP implies that for any diagram D, we are in exactly one of the following cases:  ). Therefore, there is exactly one way to meet the premises of the only rule that can reduce D to get a reduction with right-hand side (c, p). These premises completely determine the conclusion of the rule, so Proposition 5 holds for D.
If D = D 1 ⊗ D 2 with D 1 : n 1 → n 1 and D 2 : n − n 1 → n − n 2 , let (c, p) ∈ {→, ↑} × [n]. If p < n 1 , then by induction hypothesis there exist unique (c , p ) ∈ {→, ↑} × [n 1 ] and U ∈ C q×q such that (D 1 , c, p) U = ⇒ (c , p ), so that there is exactly one rule that allows us to reduce (D, c, p) (Rule ⊗1), and exactly one way to meet its premises, so Proposition 4 holds for D. If p ≥ n 1 , then by induction hypothesis there exist unique (c , p ) ∈ {→, ↑} × [n − n 1 ] and U ∈ C q×q such that (D 2 , c, p − n 1 ) U = ⇒ (c , p ), so that there is exactly one rule that allows us to reduce (D, c, p) (Rule ⊗2), and exactly one way to meet its premises, so Proposition 4 holds for D.
Similarly, if p < n 1 , then by induction hypothesis there exist unique (c , p ) ∈ {→, ↑}×[n 1 ] and U ∈ C q×q such that (D 1 , c , p ) U = ⇒ (c, p), so that there is exactly one rule that allows us to reduce D and get (c, p) (Rule ⊗1), and exactly one way to meet its premises, so Proposition 5 holds for D. If p ≥ n 1 , then by induction hypothesis there exist unique (c , p ) ∈ {→, ↑} × [n − n 1 ] and U ∈ C q×q such that (D 2 , c, p − n 1 ) U = ⇒ (c , p ), so that there is exactly one rule that allows us to reduce D and get (c, p) (Rule ⊗2), and exactly one way to meet its premises, so Proposition 5 holds for D.
By = ⇒ (c 1 , n) and (c 1 , n) = (c 1 , n) we have (c 3 , p 3 ) = (c 1 , n). Therefore, we cannot have p 3 = n, so p 3 < n and then there is exactly one reduction from D with right-hand side (c 0 , p 0 ), which comes from applying Rule T 2 . So Proposition 5 holds for D.
To finish proving the result, we have to check that two diagrams equivalent modulo the axioms of traced PROP have the same path semantics. To do this, it suffices to check for each of the axioms given in Figure 2 that both sides have the same operational semantics, which is straightforward.

B.1.2 Proof of Proposition 8 and Theorem 9
We first prove the following three lemmas: Lemma 34. Let n ≥ 0 and f ∈ S n+1 , and let τ be the permutation and U c,p the family of matrices, such that f = |c, p, y → |τ (c, p) ⊗ U c,p |y . For any (c, p, y (|c, p, y ) has at most one nonzero term (exactly one if f is injective), of index k 1 − 1, where k 1 is the smallest k ≥ 1 such that τ k (c, p) ∈ {→, ↑} × [n], or equivalently, the smallest k ≥ 1 such that f k (|c, p, y ) ∈ H n . Moreover, we have k 1 ≥ 3.

Proof of Lemma 35.
Well-definedness is a direct consequence of Lemma 36. Given f ∈ S n+1 , by Lemma 36 there exist a family of matrices V c,p such that . What we have to prove is that τ * is a permutation, that is, that it is a bijection.

B.1.2.1 Proof of Proposition 8
First, we do not assume the axioms of traced PROP and we prove by structural induction that for any diagram D : n → n, D is well-defined and in S n .
If D = , , ¬ , or , then this is a direct consequence of the definition of . . If D = D 2 • D 1 , then by induction hypothesis, D 1 and D 2 are well-defined and in S n . By definition we have D = D 2 • D 1 , and it is easy to see that S n is closed under composition.
If D = D 1 ⊗D 2 , with D 1 : n 1 → n 1 , then D 2 : n−n 1 → n−n 1 and by induction hypothesis, D 1 and D 2 are well-defined and we have D 1 ∈ S n1 and D 2 ∈ S n−n1 . It is easy to see that for any f ∈ S m and g ∈ S k we have f g ∈ S m+k , so that D := D 1 D 2 ∈ S n . If D = T r(D ), then by induction hypothesis, D is well-defined and in S n+1 . By Lemma 35 this implies that, D := T ( D ) is well-defined and in S n .
The last thing to prove is (still not assuming the axioms of traced PROP) that two diagrams that are equivalent modulo the axioms of traced PROP have the same denotational semantics. For this it suffices to remark that the proof of Theorem 9 does not need to assume the axioms of traced PROP, so Theorem 9 still holds if we do not assume them. Then, since two diagrams equivalent modulo these axioms have the same path semantics (see Appendix B.1.1), that is, the same permutation τ D and matrices [D] c,p , by (9) they have the same denotational semantics.

B.1.2.2 Proof of Theorem 9
We proceed by structural induction on D. If On the other hand, by induction hypothesis, we have D 1 = |c, p, y → |τ D1 (c, p) ⊗ [D 1 ] c,p |y and D 2 = |c, p, y → |τ D2 (c, p) ⊗ [D 2 ] c,p |y . Therefore, for any (c, p, y) ∈ {→, ↑} × [n] × [q] we have D (|c, p, y ) = D 2 ( D 1 (|c, p, y ) ] c,p |y . So the result holds for D. If D = D 1 ⊗ D 2 with D 1 : n 1 → n 1 , then on the one hand, we have  Let ∼ be the relation such that D 1 ∼ D 2 if and only if D 1 = D 2 and ≈ be the relation such that D 1 ≈ D 2 if and only if PBS D 1 = D 2 . By definition, ≈ is the smallest congruence preserving Equations (1) to (10). It is clear that ∼ is a congruence, so it suffices to prove that it preserves Equations (1) to (10) too. This can be done easily by using the graphical way to compute the denotational semantics provided by Theorem 9.

B.2.2 Normal forms B.2.2.1 Proof of Lemma 17
We have to show the following result: Lemma 38. For any diagram N : n → n in normal form and any diagram g of the form We proceed by induction on n.
If n = 0, then there is no such g so the result trivially holds. If n ≥ 1, we write N in the form We call these two forms type A and B respectively.
By induction hypothesis we only have to prove that g • N can be put in the form To prove this, we proceed by case distinction: If h = , then g • N = N , so there is nothing to do. If h = ¬ , then we slide it through σ j (σ k and σ j if N is of type B), if it does not arrive on the last wire if N is of type A, or one of the last two wires if N is of type B, then we get the desired form with D = ( ⊗i ) ⊗ ¬ ⊗ ( ⊗n−i −2 ) if it arrives on the last wire (resp. on one of the last two wires), then it merges with the on its wire and changes its value: if is then h simply takes its place, and if is ¬ then the two negations cancel by the following equation, that we prove below to be a consequence of the axioms of the PBS-calculus: If h = E(U , V ), then we slide it through σ j (σ k and σ j if N is of type B), if it does not arrive on the last wire if N is of type A, or one of the last two wires if N is of type B, then we get the desired form with if it arrives on the last wire (resp. on one of the last two wires), then it commutes with the on its wire, trivially if is , and by the following equation if is then, if N is of type B, it passes through the beam splitter by one of the following two equations: finally, the top part becomes part of D, and the bottom part merges with the E(U, V ) from N by the following equation: If h = , then by manipulating the wires according to the axioms of traced PROP, we can write g • N in one of the desired forms, with D being a permutation of the wires (that is, a composition of tensor products of and ). If h = then we look at the indices i 1 and i 2 of the wires to which h is connected on the other side of σ j (on the other side of σ k • (σ j ⊗ ) if N is of type B). The wire i 1 is connected to the top wire of the beam splitter and the wire i 2 to the bottom wire of the beam splitter.
If i 1 , i 2 < n − 1 in the case of type A (i 1 , i 2 < n − 2 in the case of type B), then i 2 = i 1 + 1 and we can slide the beam splitter across σ j (σ k and σ j in the case of type B) to put N in the desired form with If N is of type A and i 2 = n − 1, then by manipulating the wires we can write g • N in the form where D 1 and D 2 are permutations of the wires. Then we apply the following equation: the ¬ on the left is composed with D 1 to give us D. Finally, we get the desired form by manipulation of the wires. If N is of type A and i 1 = n − 1, then by manipulating the wires, and applying once the following equation : where D 1 and D 2 are permutations of the wires. Then we proceed as in the previous case. If N is of type B, i 1 < n − 2 and i 2 = n − 2, then by manipulating the wires we can write g • N in the form where D 1 and D 2 are permutations of the wires. Then, according to the between the two beam splitters, we use one of the following two equations: Immediately in the second case, or after a few manipulation of wires in the first case, we get the desired form.
If N is of type B, i 2 < n − 2 and i 1 = n − 2, then by manipulating the wires and using once Equation (17), we can write g • N in the same form as in the previous case. Then we proceed in the same way.
If N is of type B, i 1 < n − 2 and i 2 = n − 1, then by manipulating the wires we can write g • N in the form where D 1 and D 2 are permutations of the wires. Then if the between the two beam splitters is , then we apply the following equation: if the between the two beam splitters is ¬ , then we proceed as follows: = ¬ ¬ ¬ which gives us the desired form after some manipulation of wires. If N is of type B, i 2 < n − 2 and i 1 = n − 1, then by manipulating the wires and applying Equation (17) we write g • N in the same form as in the previous case, and we proceed in the same way. If N is of type B, i 1 = n − 2 and i 2 = n − 1, then by manipulating the wires, we can write g • N in the following form: then we apply one of the following equations: In the three cases, this gives us the desired form, after a few manipulation of wires if necessary.
If N is of type B, i 1 = n − 1 and i 2 = n − 2, then by manipulating the wires and applying Equation (17) once, we can write g • N in the same form as in the previous case and proceed in the same way. This finishes the case distinction.

B.2.2.2 Proof of Lemma 18
We write N in the form As in Section B.2.2.1, we call these two forms type A and B respectively.
We proceed by case distinction: If N is of type A and j = n − 1, then we apply one of the following two equations, that we prove below to be consequences of the axioms of the PBS-calculus: If N is of type A and j = n − 1, then we slide the E(U, V ) and the through the trace and σ j , then integrate them to N by Lemma 38. Finally, we remove the trace by yanking, which gives us a normal form after a few additional manipulation of wires. If N is of type B and k = n − 1, then we apply one of the following two equations: then we conclude by Lemma 38 and manipulation of wires. If N is of type B, k < n − 1 and j = n − 2, then we apply one of the following two equations: then we conclude by Lemma 38 and manipulation of wires. If N is of type B, k < n − 1 and j < n − 2, let D represent E(U, V ). We proceed as follows: It remains to prove Equations (35) to (40).

B.2.3 Proof of Theorem 21
We prove for each equation that it is not a consequence of the others in a dedicated lemma. For Equations (1), (2), (5) and (6), the proof follows a common pattern: we introduce a new semantics [[[.]]] and check that it preserves every equation except the one that we want to prove to be independent from the others. In each case, Lemma 41 gives us that the consequences of the preserved equations are preserved too, which proves that the unpreserved equation is not a consequence the others.
By using the graphical characterisation of the denotational semantics adapted to [[[.]]], it is easy to check that Equations (1) and (3) to (10) (2) is not a consequence of them.

Proof. Since Equation
Given a diagram D : n → n, let us say that a wire in D is used if there exists c ∈ {→, ↑} and p ∈ [n] such that an input photon with classical polarisation c and position p passes through this wire. Let us define d(D) as the product of all determinants of the matrices labelling the gates that are on used wires of D.
Let us fix a diagram D and consider the effect of applying the axioms inside it. It is easy to check that all axioms of traced PROP, as well as Equations (1), (2), (5) and (8) to (10) preserve the gates of D and the fact that their wire is used or not. Equation (7) can only add or remove gates on unused wires. Equation (4) adds or removes V on an unused wire and does change the fact that the wire of U is used or not, indeed, in the patterns on both sides of the equation, the wire of U is used if and only if it is possible to have a photon with polarisation ↑ arrive at the input of the pattern. Applying Equation (6) replaces U and V by V U (or V U by U and V ) on a given wire, which does not change d(D). Thus, applying Equations (1), (2) and (4) to (10) does not change d(D). On the other hand, we have d ( U ) = det(U ) and d U U = det(U ) 2 . Hence, as soon as det(U ) = 1, Equation (43) changes d(D), so that it is not a consequence of (1), (2) and (4) to (10), which is what we wanted to prove. (4) is not a consequence of Equations (1) to (3) and (5) to (10).

Lemma 45. For any U , Equation
Proof. This is clear, because Equations (1) to (3) and (5) to (10), as well as the axioms of traced PROP, preserve the parity of the total number of and ¬ in a given diagram, whereas Equation (4) changes this parity. (5) is not a consequence of Equations (1) to (4) and (6) to (10).  (4) and (6) to (10) are preserved, and Equation (5) is not preserved because its left-hand side is interpreted as the identity whereas its right-hand side is interpreted as σ . By Lemma 41, this implies that Equation (5) is not a consequence of Equations (1) to (4) and (6) to (10).

Lemma 48. For any U , Equation
Proof. This is clear, because Equation (7) is the only one that allows us to make a nonempty diagram equivalent to the empty diagram. (8) is not a consequence of Equations (1) to (7), (9) and (10).

Lemma 49. Equation
Proof. This is clear, because Equation (8) is the only one that allows us to make a diagram without beam splitters equivalent to a diagram containing beam splitters. (10) is not a consequence of Equations (1) to (9).

Lemma 50. Equation
Proof. It suffices to remark that Equation (10) is the only one that allows us to change the parity of the number of ¬ in a diagram.
To prove that Equation (9) is not a consequence of the others, we will need to talk about sub-diagrams in a context where not all axioms of traced PROP are assumed. Although the notion of sub-diagram is clear in a traced PROP, it becomes less obvious when some axioms are missing. This is why we give a formal inductive definition of it: Definition 51. We define the notion of sub-diagram inductively as follows. Given two diagrams d and D, we say that d is a sub-diagram of D if we at least one of the following properties is satisfied (up to the currently assumed axioms, which are the axioms of a traced PROP in most of this paper but will be the axioms of a PROTWEB in the proof of Lemma 52): d = D there exists two nonempty diagrams D 1 and D 2 such that D = D 2 • D 1 and d is a sub-diagram of D 1 or a sub-diagram of D 2 there exists two nonempty diagrams D 1 and D 2 such that D = D 1 ⊗ D 2 and d is a sub-diagram of D 1 or a sub-diagram of D 2 there exists a diagram D such that D = T r(D ) and d is a sub-diagram of D .
Proof. Let us first make two remarks. First, since Equation (9) does not contain gates, if it is a consequence of the other equations, then it is a consequence of these equations where all U and V are instantiated by I. Indeed, all of these equations that contain gates are still true when all U and V are instantiated by I. Hence, given a valid derivation of Equation (9) from the others, by replacing every unitary matrix by I in this derivation we get a valid derivation of Equation (9).
Second, by Equation (1), being a consequence of Equations (1) to (8) and (10) where all U and V are instantiated by I is equivalent to being a consequence of these equations where the gates have been removed (except in Equation (1)). That is, being a consequence of the following equations: Equation (1) is now useless since it only allows us to create and remove I gates without changing anything else, and neither the other equations nor Equation (9) contain gates. Equations that have become an instance of reflexivity are now useless too. Finally, Equation (4') can be simplified through Equations (8) and (7') into Equation (46). Thus, what we have to prove is that Equation (9) is not a consequence of the following equations: In the rest of the proof, we no longer assume the yanking and inverse law axioms, but we consider the corresponding equations instead: We have to prove that Equation (9) is not a consequence of Equations (46), (5), (7'), (8), (10), (y) and (σσ), still assuming the other axioms of the traced PROP, which by Lemma 33 are the axioms of a PROTWEB.
We also consider the notion of sub-diagram with respect to the axioms of a PROTWEB, that is, in Definition 51, the conditions are considered up to these axioms. Intuitively, a sub-diagram in this sense is a part of a diagram that can be separated from the rest of the diagram by drawing a box around it.
Let us say that a diagram is circle-free if it does not have nonempty 0 → 0 sub-diagrams. Intuitively, a 0 → 0 sub-diagram in the context of the PROTWEB is represented graphically as a union of connected components, which cannot be reached by a photon and do not affect the semantics of a diagram.
We consider the following set of rewriting rules on the set of gate-free diagrams: for every diagram D with a circle-free, nonidentity sub-diagram d : 2 → 2 that we can slide along its two wires inside D, by using the axioms of the PROTWEB, in a constant direction and make it come back to the initial point, without having to use naturality of the swap or dinaturality to move anything else than d while doing so → It is easy to see that these rules preserve the semantics.
Remark 53. Any gate-free 1 → 1 diagram is interpreted as Id or ¬ , so it can be reduced to Id or ¬ by first applying Rule (1) repeatedly to remove all its 0 → 0 sub-diagrams, then applying Rule (2) or (3).
Since all diagrams have their number of input wires equal to their number of output wires, the axioms of the PROTWEB do not change the number of , , ¬ or of trace wires in a diagram, so these numbers are well-defined for a given diagram. This allows us to define the level of a diagram as a tuple (b, x, n, t), where: b is the number of x is the number of n is the number of ¬ t is the number of trace wires.
It is easy to check that each of the rewriting rules strictly decreases the level, according to the lexicographic order. Since the lexicographic order on N 4 is well-founded, this implies that the rewriting system is strongly normalising.
Let us prove that the rewriting system is confluent. Because of strong normalisation, it suffices to prove that it is locally confluent. Let → * be the reflexive transitive closure of →.
Let D be a diagram and let D → D 2 be two reduction steps, where (a) and (b) are the respective rules applied. We have to prove that there exists a diagram D such that D 1 → * D and D 2 → * D .
If the two patterns in D that are transformed by (a) and (b) do not overlap, then after applying (a) to the first pattern or (b) to the second one, we can still apply the other rule to the other pattern and the final result does not depend on the order in which (a)  In the following case distinction, we assume that the patterns concerned by (a) and (b) overlap.
It is easy to see that if (a) is (1), (2) or (3) and (b) is among Rules (5) to (11), then the only way the concerned patterns in D can overlap is that the pattern concerned by (b) is included in this of (a). In this case, on the one hand, (a) transforms its pattern into , Id or ¬, and on the other hand, the effect of applying (b) is to transform the pattern of (a) into a semantically equivalent diagram (which is not , Id or ¬ because it contains at least a trace), which can then be transformed into , Id or ¬ by applying (a). Since the rules preserve the semantics, the final sub-diagrams obtained in each case are the same. Therefore, D 2 (a) → D 1 . Of course, the same argument applies with (a) and (b) exchanged. (2) or (3), then since the pattern concerned by (b) does not contain any 0 → 0 sub-diagram, it is necessarily included in the pattern concerned by (a), which, after applying (b), can still be transformed into the empty diagram by applying (1). Therefore, D 2
If both (a) and (b) are Rule (1), then the union of the two patterns concerned by (a) and (b) is a 0 → 0 sub-diagram of D. Applying (a) or (b) does not change the fact that it is of type 0 → 0, so that right after that we can transform it into the empty diagram by applying Rule (1) (unless it has already become empty in which case there is nothing more to do). This gives us the desired D If both (a) and (b) each are Rule (2) or (3), then the union of the two concerned patterns can be written in the form d 2 • d • d 1 in such a way that, up to exchanging the roles of (a) and (b), the pattern concerned by (a) is d • d 1 and the pattern concerned by (b) is d 2 • d. Therefore, after applying (a) or (b), we can apply Rule (2) or (3) to transform the resulting whole sub-diagram into id or ¬, and since the rules preserve the semantics, the result is the same regardless of whether (a) or (b) was applied. This gives us the desired D .
If (a) is Rule (4), then: if (b) is Rule (1), then since d is circle-free, it does not intersect the pattern concerned by (b). Therefore, the situation is the same as when the two patterns do not overlap and there exists D such that D 1

B.3.3 Proof of Lemma 27
We proceed by structural induction on D.
If D = , , ¬ , or , then D does not contain any gate and for any (c, p) we have det([D] c,p ) = 1, so with the usual convention that the empty product is equal to 1, the result holds.
If D = U , then we have |D| =