{'fraction_non_alphanumeric': 0.03453028014508892, 'fraction_numerical': 0.0060416965260244974, 'mean_word_length': 4.236951501154734, 'pattern_counts': {'":': 0, '<': 3, '<?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': 30, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Generalised Proof-Nets for Compact Categories with Biproducts

Just as conventional functional programs may be understood as proofs in an intuitionistic logic, so quantum processes can also be viewed as proofs in a suitable logic. We describe such a logic, the logic of compact closed categories and biproducts, presented both as a sequent calculus and as a system of proof-nets. This logic captures much of the necessary structure needed to represent quantum processes under classical control, while remaining agnostic to the fine details. We demonstrate how to represent quantum processes as proof-nets, and show that the dynamic behaviour of a quantum process is captured by the cut-elimination procedure for the logic. We show that the cut elimination procedure is strongly normalising: that is, that every legal way of simplifying a proof-net leads to the same, unique, normal form. Finally, taking some initial set of operations as non-logical axioms, we show that that the resulting category of proof-nets is a representation of the free compact closed category with biproducts generated by those operations.


Logic, Processes, and Categories
Birkhoff and von Neumann initiated the logical study of quantum mechanics in their 1936 paper [BvN36]. They constructed a logic by assigning a proposition letter to each observable property of a given quantum system, and studied negations, conjunctions, and disjunctions of these properties. The resulting lattice is non-distributive, and so the heart of what is called "quantum logic"is the study of various kinds of non-distributive lattices. These traditional quantum logics suffer from a number of defects. Firstly, they are monolithic: there is no way to derive the properties of a composite system from the properties of its parts. Each system has its own associated lattice which can only rarely be related to those of other systems. Further, these systems are seen statically: a system that undergoes some dynamical change is a new system. Finally, the failure of compositionality is connected with the fact that quantum logic has no decent notion of implication [Sme01]; hence we have a logic which has a notion of validity, but no concept of inference or proof.
These limitations form a serious obstacle to the use of Birkhoff-von Neumann-style quantum logic to study interacting quantum systems. If by "system" we understand the ubiquitous qubit, then it is precisely such interactions which form the basis of quantum informatics. Indeed, the principal concern of the computer scientist †-how to soundly construct large systems from smaller ones-is exactly where quantum logic is weakest.
In this article I will describe a very different kind of logic which can address these questions. This logic is called tensor-sum logic and it shares many features with linear logic [Gir87a], which has been widely studied in computer science and structural proof theory.
We proceed in accordance with an old tradition in computer science, that of linking computational systems and logics, of claiming that a certain logic "is the same as" some formal computing machine. The archetype of this approach is the Curry-Howard correspondence between intuitionistic natural deduction [Gen35,Pra65] and the simply-typed λcalculus [CF58,How80]. The basic insight is that the inference rules of the logic are essentially the same as the constructors used to form a λ-term. The valid types of the λ-calculus are nothing more than the theorems of the logic, and more importantly every proof represents a λ-term. We can thus view the logic itself as a computational system, with the important proviso that the objects of interest are the proofs and not the theorems. This correspondence is not just skin deep. Recall that the β-reduction relation between λ-terms expresses the execution behaviour of the calculus; we consider terms to be computationally equivalent when they reduce to the same β-normal form. This dynamical aspect of the λ-calculus corresponds exactly to the normalisation procedure for natural deduction proofs or, in the sequent calculus setting, to the cut-elimination procedure [Gen35]. In our presentation of tensor-sum logic we will take this correspondence as given, and treat the proof theoretic presentation as a computational system in its own right. The normalisation procedure gives the computational dynamics.
There is a further correspondence that we engage with rather more seriously: that between the proofs in a given logic and the arrows in a particular class of categories [Lam68,Lam69]. We can equate the propositions of a logic L with the objects of a category C; for each proof of, say, a proposition B from a premise A, we define a corresponding arrow f : A → B in the category. Stated so blandly, we have little structure to work with, so we go further, and demand that the logical connectives are represented by functors on C. The natural transformations between these functors then give rise to the inference rules of the logic. In this way an arrow in C may be constructed for each proof in L; we say that C is a denotational model of L if, whenever two proofs share the same normal form, they have equal denotations in C. The categorical model gives an extensional account of the computational dynamics represented in the term language. The general schema of this tripartite relation is shown in To return to our earlier example, the simply-typed λ-calculus forms such a triple with intuitionistic natural deduction and the class of Cartesian closed categories [LS86]. Another example is provided by intuitionistic multiplicative linear logic [Gir87a]; this logical system corresponds to the linear λ-calculus and to the class of *-autonomous categories [Bar79,Bar91]. The pattern is quite general, and more examples can easily be found.
This relationship between a logic and its categorical models can be made exact. In the above description we embedded the connectives and inference rules of L into C using only functors and natural transformations: the logical structure is agnostic with respect to the concrete elements of the category. Hence any category with the requisite functors can provide a model, up to some assignment of the basic proposition let-ters. Of course such a category may well contain other objects or arrows which do not correspond to anything in the logic we are trying to model. To make the correspondence exact we must be able to translate from the free category (with appropriate structure) faithfully back to our logic. That is, we must find an injective translation from the arrows of C onto the cut-free proofs of L. In the case of our generalised proof-nets, that is indeed possible, but for a simpler example, consider the simply-typed λ-calculus with just one ground type; then the category of its terms is the free Cartesian closed category generated by the category 1, which has only one object, and one identity arrow.
The choice of generator can be rather important. By choosing a discrete category (i.e. a set) the resulting logic will have that set as its propositional variables. By choosing a category with non-trivial arrows, we introduce non-logical axioms: if cut-elimination for the resulting logic is to be retained we must lift the composition operation of C into the cut-elimination procedure of L itself. If other equations between arrows are required these too must be hoisted into the logic. In the case we consider here, the situation is even worse: we will take as a generator a compact symmetric polycategory [Dun06]. This esoteric creature will be described in a later section, but for now we note that the intricacy of the required composition forces the adoption of the proof-net formalism, an illustration of the power of graphical methods over conventional syntax.
The development in the following sections will be the reverse of the exposition above. We first describe the mathematical basis of quantum computation in its concrete setting-finite dimensional Hilbert spacesthen we identify certain structures of the category fdHilb which are the essential features for carrying out quantum computation. Next we present the syntax of tensor-sum logic, and finally prove that the category of generalised proof-nets is the free compact closed category with biproducts generated by a compact symmetric polycategory.
Prior Work The original formulation of quantum mechanics in terms of compact closed categories with biproducts was due to Abramsky and Coecke [AC04]. An early attempt to formalise quantum computations in terms of proof-nets for MLL was [Dun04]. The first description of a logic based on compact closed categories and biproducts was given by Abramsky and the author in [AD06], however this logic is essentially restricted to quantum systems with only bipartite entanglement. This restriction was lifted in [Dun06] via the use of polycategories, although only the multiplicative fragment of the logic was treated. The present article is essentially a fusion of the previous two: giving a complete presentation of two-sided proof-nets with generalised axioms, and both the tensor and sum connectives. A notable distinction between the treatment of the biproduct here as compared to that of [AC04] is that here the biproduct is freely generated, hence the our treatment is closer to that of [Sel04]; we will discuss the vexed position of this connective at the end of Section 1.1.2.

Quantum Mechanics Concretely, and Abstractly
The main work of this article is to characterise the structure of certain kinds of category in terms of proof-nets. The particular categories we are interested in are compact closed categories with biproducts, and in the next section we'll go into considerable detail defining, characterising, and giving some of the basic properties of such categories. In this section we describe, at a more intuitive level, how the structure relates to quantum mechanics and quantum computation in particular.
We start with a schematic description of quantum mechanics. Since we are interested in quantum computation, we will restrict ourselves to quantum systems with finite dimensional state spaces. Consider the following axioms.
(i) To each quantum system we associate a finite dimensional Hilbert space, its state space; the possible states of the system are unit vectors in the state space, modulo a global phase factor. (ii) If two systems are combined, then their joint state space is the tensor product of the two state spaces. (iii) Measuring a quantum system is non-deterministic; possible outcomes are the eigenvectors of some self-adjoint operator on the state space, and the probability of observing a particular outcome depends on the inner product of the current state and the eigenvector for that outcome. After the measurement the state is updated to match the observed vector †, assuming it is not destroyed by the act of measuring. (iv) For any discrete time step, the next state of the system is determined by a unitary map on its state space.
Of course, we have omitted some important details, but the above axioms approximate the level of abstraction of our categorical formalisation.
The first thing we should note that the fdHilb, the category of finite dimensional Hilbert spaces and linear maps, is the "natural" category in which to formalise the above axioms ‡. The second point is that fdHilb is compact closed and has biproducts. Thirdly, the above axioms can be rephrased in terms of the categorical structure alone.
Before showing how the ingredients of the axioms translate into categorical terms, let's dispose of some unnecessary baggage. Consider a linear map ψ : C → H. Since it is linear, and its domain is onedimensional, its value is fixed by its value on 1, hence maps of this type are in 1-1 correspondence with vectors of H. Hence we can forget about vectors and talk only of linear maps. Now consider measurements. There are three parts to a quantum measurement: the non-deterministic possibilities, the calculation of the probabilities, and the updated state. We will deal with these in reverse order. The new state of a measured system depends only on which outcome i of the measurement happened, hence it is just a new state |φ i , with no particular relation to the old one. Of course, the measurement process may destroy the system, in which case there is no new state. To calculate the probability of seeing outcome i when we are in state |ψ we must calculate the inner product φ i | ψ . This process too can be seen as a linear map, namely the projection map φ i | : H → C; when composed with |ψ this yields the inner product. Hence the state transformation associated to the ith outcome of some measurement is described by the map: Note that this is desired transformation even in the case when only part of a composite system is measured. For the purposes of this work, calculating the probabilities is not so important, but the transformation of the state is essential.
Finally let's consider the non-deterministic aspect of measurement. The main point is that there several possible outcomes and we know which one happened. Suppose we perform a measurement with two outcomes; we can view this process as map of type H → H ⊕ H ‡ As the first and last axioms suggest fdHilb is actually too big: it contains vectors and maps which do not correspond to anything in quantum mechanics. The general program of describing quantum mechanics in categorical terms aims to find the minimal structure required.
where the two sides of the direct sum correspond to the two "possible worlds" induced by the two outcomes of the measurement. One can then represent conditional operations by acting on only one subspace or the other; for example f ⊕ g behaves as the linear map f : H → H if the first outcome was observed, and g : H → H if the second was observed.
How then can we write the axioms of quantum mechanics in the language of compact closed categories and biproducts? Firstly, compact closed categories are equipped with a tensor product, and this tensor product has a neutral element I. In fdHilb the tensor product is simply the usual Kronecker product, and its neutral element is the base field, namely C. This gives us the first two axioms: • To each quantum system we associate an object A, its state space; the possible states of the system are given by arrows ψ : I → A. • If two systems with state spaces A and B respectively are combined, then their joint state space is A ⊗ B.
In fdHilb the biproduct is the direct sum of Hilbert spaces, and this will allow the formalisation of measurements.
• An n-outcome measurement of a quantum system whose state space is A is represented by an arrow where each of the the projections π i • m : A → B i factors as This is very general notion of measurement. The common cases are when B i = I and the original system is destroyed; and, when B i = A when the original system is preserved. Since we are interested in formalising as much of quantum mechanics as possible within one category we will not restrict state transformations to unitary evolutions; note that a measurement is a valid transformation of a quantum state which is not unitary. Hence the last axiom is simply the following.
• A quantum system A may transform to another system B by means of any arrow f : A → B.
We have not yet mentioned the role of the compact structure of the category. While not required to paraphrase the axioms, the compact structure plays an important role in capturing quantum phenomena.
Recall that the tensor product of two vector spaces contains points, Ψ : I → A⊗B which cannot be factored into a pair of vectors ψ 1 : I → A and ψ 2 : I → B. The such quantum states are called entangled and they a central role in quantum computation. The compact structure guarantees the existence of certain entangled states, namely Bell states for every finite dimensional Hilbert space: If A is two-dimensional, i.e. a qubit, then the corresponding vector is Further more, the compact structure also provides a projection onto this state hence we can define measurements on Bell states. These two operations will allow many more entangled states to be defined. This completes our impressionistic description of how quantum mechanics may be formalised in the categorical setting. Before moving on, it worth pointing out what has been excluded from our formalisation. Perhaps the most striking omission in moving between the concrete axioms and the abstract is the concept of unitarity.
The abstract formulation of quantum mechanics described here is derived from that introduced in [AC04] which uses strongly compact closed categories. Also called †-compact, these categories are equipped with a contravariant involutive functor which sends each map f to its adjoint f † , and has no effect on objects. This functor can then be used to define unitarity and the inner product. In this article, we focus on freely constructing the compact closed and biproduct structure from some underlying category of generators. One could consider the case when these structures cohere with the (·) † operation, giving a †-compact category with †-biproducts; however the only difference here between the †-structure and the original is that the structural isomorphisms are required to be unitary. That is to say that the only new maps which are introduced are the adjoints of the generators. Hence we can simply enlarge the class of generators beforehand, and thereafter ignore the †-structure. Of course, when working on concrete examples it is important to be aware of the adjoints, and the equational theory of the generators more generally, but that is not the focus of the present article. The other important deviation from usual quantum mechanics is that we have been extremely liberal about measurements. In particular we do not make any restriction on the number of outcomes a measurement may have. Of course, in quantum mechanics the outcomes are the spectrum of some operator, and hence are bounded by the dimension of the space. Considering these issues would take us too far afield but [AC04] has one approach; a more recent categorical treatment of quantum observables is found in [CD08]. In any case, it seems unlikely that the structure of quantum measurements-being fundamentally connected to the bases of the underlying space-will yield to a description in terms of natural transformations of some functors.

Some Remarks on the Biproduct
In their original paper [AC04] Abramsky and Coecke used the biproduct of fdHilb in two roles: firstly, to encode classical branching, as described above; and secondly, to construct bases for the underlying space. In particular, they define state preparations and destructive measurements as isomorphisms of the forms base : This second use of the biproduct has been criticised by later works [Coe05a,Sel05] on two main accounts. In the original approach the composite yields the identity map, contradicting physical reality-a real experiment would transform a pure state to a mixed state, something not handled within this simple framework. More importantly, when moving from a "vector space" setting like fdHilb to a "projective" setting, such as Selinger's CPM construction or Coecke's WProj, the direct sum of the underlying space no longer yields a biproduct. The only option is to construct the biproduct as formal vectors and matrices. The works cited above show that, in the projective setting, if there is a biproduct then the scalars are essentially restricted to probabilities rather than amplitudes. The immediate consequence is that we must give up any hope of using the additive structure to encode interference effects: we are essentially restricted to a classical probabilistic setting. The approach to biproducts taken in this work is absolutely consonant with these restrictions. We construct both the multiplicative and additive structures freely, and hence the scalars are simply a (free) semiring.
The theory of processes thus produced is much like that introduced in [Sel04], based on classically controlled quantum operations.

An Example Proof-net
Sections 1.3 and 1.4 will introduce tensor-sum logic, and its proof-net notation. Since those sections will focus on the technical details of the formalism we present now an illustrative example of how proof-nets can be used to to model quantum processes.
We will describe an old favourite: the quantum teleportation protocol [BBC + 93]. The sketch of the protocol goes like this: Two parties, Alice and Bob, initially share an entangled pair of particles in a Bell state, The parties then separate, and at some later point Alice wants to send a qubit to Bob, but unfortunately she has only a classical channel. However, it is still possible to transmit the qubit by using the shared entanglement between the two parties. To proceed, Alice performs a joint measurement on the qubit she wishes to transmit together with her half of the entangled pair. She measures in the Bell basis, so her state will be projected onto one of the following vectors: These states are all entangled, and further, each of them can be produced by starting with |Bell 1 (aka η) and applying one of the Pauli operators; hence we can associate a Pauli operator to each outcome of the measurement. In order to complete the protocol, Alice transmits a classical message to Bob, saying which of the four outcomes she observed. Bob then applies the corresponding Pauli operation to his qubit and-as if by magic-it is now in the state that Alice wished to transmit. We now show how this protocol can be represented in term of proofnets using the compact closed structure and biproducts. By normalising the proof-net we will effectively simulate the execution of the protocol.
We start with a premise representing Alice's input, and a unit link, Notice the output of type ⊕ i I serves simply to indicate which outcome occurred Finally we consider Bob's correction. Since his behaviour is conditional on a classical input, he has a box with an input of type ⊕ i I as shown below.
Now we can open the box corresponding to Bob's non-determinism; this will leave us with sixteen copies of the system. We won't draw all of these copies, since twelve of them can be erased: theses are the cases the input that Bob is expecting does not match what Alice sends. We are left with: Now we simply note (and this is not a logical axiom) that X 2 = Y 2 = Z 2 = 1 so we can simply remove these maps. Hence we have the normal form: show that in every possible world, Alice has successfully formed a channel to Bob along which her state can be transmitted.
Although we presented the rewrites in the order that the steps of the protocol would be carried out, in fact our proof-nets are strongly normalising, so any order would produce the same results.
Having sketched the system, we move to the details. First the category theory, then in Sections 1.3 and 1.4 the logic.

Categorical Preliminaries
In this section, we introduce the necessary categorical structures, compact closed categories and biproducts, and present their basic properties. Much of this material is well known so proofs are omitted. Standard references are Mac Lane [ML97] and Kelly-Laplaza [KL80]; other material is derived from the author's thesis [Dun06]. Other sources are cited as needed.
Compact closed categories [KL80] are abundant throughout mathematics and computer science. Examples include Rel, the category of sets and relations, finitely-generated projective modules over a commu-tative ring and Conway games (as categorified in [Joy77]). In Hilb, the category of all Hilbert spaces, the sub-category of determined by the Hilbert-Schmitt maps is compact closed, and more generally, the nuclear maps of any tensored *-category [ABP99] for a compact closed subcategory. Of course, fdHilb, the category of finite dimensional Hilbert spaces is compact closed.
In computer science compact closed categories have been studied in the context of typed concurrency as interaction categories [AGN96]; in logic, compact closed categories are degenerate models of multiplicative linear logic [AJ94,Loa94,HS03]; in physics the category of ndimensional cobordisms, used in topological quantum field, theory is compact closed [BD95]. More examples are easy to find.
We define biproducts and investigate their basic properties in relation to compact closed categories. Categories with biproducts have been studied since the earliest days of category theory as part of the theory of Abelian categories [Mit65,ML97]. Compact closed categories with biproducts have been studied by Soloviev [Sol87]. A special case of compact closed categories with biproducts is Tannakien category [Del91]. A recent contribution is by Houston [Hou08], who proved that every compact closed category with products has biproducts.

Monoidal Categories
Definition 1 A category C is monoidal if equipped with a functor ⊗ : C × C → C, a distinguished neutral object I, and natural isomorphisms For the associativity morphism α we require that the pentagon commutes. The isomorphisms λ and ρ express the neutrality of I; we require that the following diagram commutes: In a monoidal category the equality λ I = ρ I holds and the following diagrams commute: Proof See [JS93].
Definition 3 A monoidal category is symmetric if it has a natural isomorphism Mac Lane's celebrated coherence theorem states that any formal diagram constructed from the α, ρ, λ and σ will commute. A monoidal category is called strict if the isomorphisms α, λ,and ρ are all identities. To minimise syntactic overhead we will make use of the following theorem through this section: Theorem 4 (Mac Lane) Every monoidal category C is equivalent to some strict monoidal category A.
Note, however, that the category of proof-nets constructed in Section 1.4 is not strict: we will produce non-trivial associativity and unit morphisms.

Compact Closed Categories
Let C be a symmetric monoidal category. We say that C is compact closed if every object A has a chosen dual † A * and maps are equal to 1 A and 1 A * respectively. We call η A and ǫ A the unit and counit maps.
Proposition 5 In a compact closed category we have natural isomorphisms: A compact closed category which, in addition to being strictly monoidal, has all of the isomorphisms u, v, w equal to the identity is called a strict compact closed category. Kelly and Laplaza [KL80] show that any compact closed category is equivalent to a strict one, hence we will take the isomorphisms above to be equalities whenever convenient.
Proposition 6 In a compact closed category the units and counits define dinatural transformations (see [GSS91]) We have a bijection between C(A, B) and C(B * , A * ): given f : We call f * the dual of f .

Proposition 7
The operation (−) * defines a functor C op → C, which is an equivalence of categories.
Proof We have 1 * A = 1 A * immediately from the definition of dual, and (f • g) * = g * • f * follows from a routine calculation. Taking C to be strict, we we have A * * = A, it follow from the defining property of compact closure that f * * = f , which gives the equivalence.
Since we have the equivalence between C and C op , any statement about some arrow applies equally well to its dual. In particular, results concerning units translate directly into results about counits and vice-versa.
The duality of a compact closed category gives a particularly strong form of monoidal closure. Every arrow in the category has a point which represents it, and dually a copoint. These representatives, the names and conames, will be crucial to our treatment of entangled quantum states.
Definition 8 Let f : A → B in a compact closed category C. Define the name and coname of f to be the maps f : I → A * ⊗ B and f : A ⊗ B * → I which are defined by the diagrams below.
An immediate consequence of this definition is the isomorphism of homsets Lemma 9 Let C be compact closed and suppose we have arrows then the following equations hold: We can also define partial versions of the name and coname; essentially currying and uncurrying.
Lemma 10 (Partial Names and Conames) In any compact closed category we have the following isomorphisms: Proof Since the two isomorphisms are dual, we prove only the first.
and hence GF = Id. Similarly Id = F G, which establishes the isomorphism.
Equation (1.1) essentially states that compact closed categories are indeed closed with B A = A * ⊗B. Since A * ⊗I ∼ = A * this gives immediately the following.
Hence compact closed categories are models of MLL, and in particular the linear λ-calculus; albeit, these are rather strange models equipped with only one, self-dual, tensor.
Definition 12 Let C be compact closed and define a map by setting The trace so defined makes C into a traced monoidal category in the sense of Joyal, Street, and Verity [JSV96]. Few of the properties of the trace are required here so we will not recapitulate the definition-in any case the relevant facts can be deduced from the properties of η and ǫ. We will, however, need the following lemma: a symmetric traced monoidal category; then: The partial trace defined above may be extended to a full trace over any endomorphism f : A → A by setting In fdHilb, the category of finite dimensional Hilbert spaces, this coincides with the usual trace, explicitly given by summing the diagonal elements of a matrix representation of f .

Scalars and Loops
Definition 14 In any monoidal category C the endomorphisms of the neutral element C(I, I) are called the scalars.

Lemma 15
The scalars form a commutative monoid with respect to composition.
Proof Let s, t ∈ C(I, I); then Corollary 16 For scalars s, t the composite Definition 17 Let C be a monoidal category. Given a scalar s and some arrow f : A → B define a scalar multiplication s • f by the composition: We could have defined s • f equivalently by multiplication on the left rather than on the right as above. Note that u : and hence the two definitions coincide.

Lemma 18 Each scalar s determines a natural transformation Id
Proof The top and bottom edges define s A and s B respectively: The outer squares commute due to naturality of ρ, and the middle due to the functoriality of the tensor. Hence s defines a natural transformation. Note that the middle path from A to B is the definition of s • f .

Corollary 19
The following are immediate.
Definition 20 In a compact closed category C define the dimension of an object A, to be the following composite: Of course, this is nothing more than the trace of 1 A . The presence of these non-trivial scalars gives a qualitative aspect even to freely constructed compact closed categories.

Freely Constructed Compact Closed Categories
Define the set of endomorphisms E(A) by the disjoint union and let the set of loops [A] be the quotient of E(A) generated by the the canonical map onto the loops, and for each endomorphism f write The key theorem is the following of [KL80].
Theorem 21 Let be a functor of 2n variables, let K and L be objects of B and let α : K ⇒ T and β : T ⇒ L be natural transformations with typical components given maps Taking A = B, K = L = I, α = η and β = ǫ gives a ready source of scalars in any compact closed category A; indeed this is the dimension map given in Definition 20. If the category is freely constructed these are the only non-trivial scalars. This is a consequence of the more general coherence theorem of Kelly and Laplaza. Before stating the theorem we must introduce some additional terminology, which will be also be required later in this section.
Definition 22 A signed set S is a function from a carrier set |S| to the set {+, −}. Given signed sets R and S, let R * denote the signed set with the opposite signing to R; let R ⊗ S be the disjoint union of R and S, such that |R ⊗ S| = |R| + |S|.
Definition 23 An involution is a category which is a coproduct of copies of the category 2. Given an involution σ, its object set |σ| can form a signed set by assigning − to the source and + to the target of each arrow of 2. Call σ an involution on the signed set S when this signing agrees with that of S.
Given some category A, we can construct the free compact closed category generated by A, which we call F A. The objects of the F A are constructed from those of A by repeated application of the functors − ⊗ −, (−) * and the constant I. This characterisation may be used to inductively construct a signed set S(X) corresponding to each object X of F A. Let The basic structure of arrows in F A depends upon involutions on the signed sets generated by its objects.
Theorem 24 (Kelly-Laplaza) Let A be a category; each arrow f : A → B of the free compact closed category generated by A is completely described by the following data: (ii) A functor θ : σ → A agreeing with σ on objects (i.e. a labelling of σ with arrows of A); (iii) A multiset L of loops from A.
The baroque statement of this theorem conceals its graphical content. One can view the objects of F A as lists of positively and negatively occurring objects of A, and an arrow between two such lists is simply a collection of arcs, each connecting a negative occurrence to a positive one, and labelled by an arrow of A. To compose arrows in F A we simply connect up the arcs, using the underlying composition in A.
From this point of view we can see an immediate limitation in the use of such freely generated compact closed categories to model quantum states. Recall that when we interpret processes in categorical terms, we view the objects as state spaces; hence the objects of the generating category A are the state spaces of the elementary subsystems from which our composite systems will be built. A state of a compound system, that is, an arrow ψ : I → X in F A, is thus composed of pairs of elementary systems related by some arrow from A, and each pair is unconnected to the others. Quantum informatics attaches great importance to entangled states; that is, states which cannot be broken down into their constituent parts. However the above result states that free compact closed categories can only result in bipartite entanglement, which does not suffice to describe all entangled states. To extend our reach we now introduce polycategories.

Compact Symmetric Polycategories
The reason that the free construction described above yields only bipartite states is simple. The states are based on the arrows of the underlying category A, and an arrow has exactly two ends. In order to represent multipartite states we will need generators with more than one and input and output, suggesting the need to construct the compact closed category from a category which already has a monoidal structure. However the direct route leaves open the problem of ensuring that the downstairs tensor (from the monoidal category A) and the upstairs tensors (freely generated in F A) cohere correctly. Worse, there is no reason to believe that an arrow in a monoidal category is in any sense indecomposable among its subsystems.
Fortunately there is a natural generalisation of category, a polycategory, whose arrows may have more than one object in their domain and codomain. The original notion of polycategory [Lam68,Sza75] was introduced to study classical logic, where a sequent may have multiple premises and conclusions; composition is defined by the cut-rule, so one output is connected to one input. Here we consider compact symmetric polycategories [Dun06], where composition is defined by the multi-cut rule, allowing arbitrary vectors of inputs and outputs to be composed.
Definition 25 A compact symmetric polycategory, P, consists of a class of objects Obj P and, to each pair (Γ, ∆) of finite sequences over Obj P , a set of polyarrows P(Γ, ∆). Given a non-empty sequence of objects Θ and poly-arrows we may form the composition In general there are many ways to compose the polyarrows, and many equations which must be satisfied. We will spare the reader the full definition †, and instead we will offer a theorem in the spirit of the Kelly-Laplaza result cited above, characterising the free compact closed category generated by such a polycategory. Before proceding we note the most important point about these polycategories: there is no nullary composition and no tensor product. Each input of a polyarrow has a path (not necessarily directed) to each output, and hence despite having many inputs and outputs, polyarrows cannot be decomposed into non-interacting parts.
Before we can state the representation theorem we must make some definitions.
Definition 26 A graph consists of a 5-tuple (V, E, C, s, t) where V ,E, and C are sets, respectively of vertices, edges, and circles, and s and t are maps which we call source and target. Let in(v) and out(v) be V -indexed † For the full glory of its coherence equations, and also the proof of the theorem cited, see [Dun06].
The in-degree of a vertex v is the cardinality of in(v) and the out-degree is the cardinality of out(v). The degree of a vertex is the sum of its inand out-degrees.
Definition 27 A open graph is a pair (G, ∂G) of an underlying graph G = (V, E, C, s, t) and a distinguished subset of the degree one vertices ∂G called the boundary of G; V − ∂G is called the interior of G, written I G . If a vertex x ∈ ∂G it is an outer or boundary node; otherwise it is an inner or interior node.

t), ∂G) is an open graph;
• dom Γ and cod Γ are totally ordered sets such that ∂G = dom Γ + cod Γ; As suggested by their name, the purpose of the two maps < in(·) and < out(·) is to impose a linear order on in(v) and out(v). Since the maps give a bijective correspondence between in(v), out(v) and an initial segment of the naturals, the order in N lifts, and hence we will often simply treat these sets are ordered, and write < for this ordering whenever unambiguous to do so. For simplicity, in the following we will consider a polycategory P which is freely generated from some set of basic arrows † called Arr P .
Definition 29 Given a polycategory P, an P-labelling for a circuit Γ is a pair of maps The boundary nodes perform a different role to the interior nodes. The incidence of the unique edge at a boundary vertex b defines a signing on the boundary: we say that b is positive if it has in-degree 1; and negative if its out-degree is 1. We will take the boundary vertices as labelled by objects of P rather than the corresponding identity maps, and treat the boundary as an Obj P -labelled signed set.
We denote the class of P-labelled circuits Circ(P); it forms a monoidal category in a rather natural way. The objects of Circ(P) are signed sequences of objects from Obj P . An arrow from f : A → B is defined by a P-labelled circuit whose codomain is B and whose domain is A * (i.e A with the opposite signing). Composition is defined by joining two circuits at their respective domain and codomain vertices, and erasing the vertices. The tensor product can be defined by taking the disjoint union of the circuits, and concatenating the domain and codomains. We leave the reader to fill in the details. We can now state the promised representation theorem: Theorem 30 Circ(P) is the free compact closed category generated by the compact symmetric polycategory P.
Since categories are a special case of polycategory (where all the arrows are between singleton sequences) we can ask: what is Circ(P) when P is just a normal category? In this case, Circ(P) is exactly the same as F P as per Kelly-Laplaza.
One way to understand the generalisation in going from a category of generators to a polycategory of generators is by considering the case with only one ground type. If we have a category with just one object, we can view its arrows as evolutions of this state space. On the other hand, if we have a polycategory with a single object, the arrows are in some sense interactions between systems of that type, possibly fusing or splitting, producing a different number of systems than began the interaction. By moving to the compact closed category generated by a polycategory of interactions we avoid the restriction to bipartite states mentioned earlier.
This concludes the multiplicative structures, now we move onto the additives.

Zero Objects
Definition 31 In any category C a zero object is an object, denoted 0, which is both initial and terminal.
By its initiality, there is a unique map from 0 to every object, and dually there is a unique map from each object to 0. Hence there is unique map between every pair of objects A and B. This map is called the zero map and denoted 0 A,B . Since 0 is initial and terminal any map composed with a zero map is again a zero map; the zeros form a two-sided ideal with respect to composition among the arrows C. Hence the following diagram commutes: which makes the family 0 A,B natural in both A and B.
A useful family of arrows in a category with 0 is the Kronecker delta δ ij : A i -A j , defined for all pairs of objects A i , A j as Proof Note that the composite is equal to 0 0,0 , which by uniqueness is equal to 1 0 . Thus ! A • ! A = 1 A and ! A • ! A = 1 0 , which gives the isomorphism.
Proposition 33 Let C be a monoidal closed category with a zero object.
Proof Since C is closed, Taking B = A ⊗ 0 implies 1 A⊗0 = 0, and hence the result follows.
Monoidal closure is required; if we take the tensor to be a coproduct, e.g direct sum of vector spaces, it is clear that the isomorphism does not hold.
Corollary 34 Given f : If the zero object is also the neutral object for the tensor, then the entire category collapses to a single object via A ∼ = A ⊗ 0 ∼ = 0. So any Cartesian closed category with zero is trivial. Note that in a compact closed category C with a terminal object 1, by duality 1 * is initial. If the terminal object is the monoidal unit then the isomorphism I ∼ = I * makes I the zero object, and hence the category collapses.
Proposition 35 If C is compact closed with respect to a product then it is trivial.

Biproducts
In any category C with finite products and coproducts every map has a "matrix" representation (f ij ) where each f ij is given by the composite with in i and π j the appropriate injections and projections. Supposing that C also has a zero object there is canonical map : A i -A i whose matrix is the identity = (δ ij ).

Definition 36 A category C has finite biproducts if it has finite products and coproducts, such that
• the unique map 0 -1 is invertible; and • the canonical map : A B -A B is an isomorphism for all objects A, B.
If C has biproducts, for all objects A and B, there is a unique (upto isomorphism) object A ⊕ B and maps such that (A⊕B, π 1 , π 2 ) is a product and (A⊕B, in 1 , in 2 ) is a coproduct. A choice of A ⊕ B for every pair of objects makes − ⊕ − into a functor C × C -C whose action on arrows f 1 ⊕ f 2 is given by or alternatively Lemma 37 In a category with biproducts we have the following natural isomorphisms: Proof All these isomorphisms hold for products (and also coproducts) hence they hold for the biproduct.
We have natural diagonal and codiagonal maps, It is useful to note the equations Definition 38 Let f, g : A -B; then define f + g as the composite Proposition 39 In a category with biproducts C, the addition of Definition 38: • makes each hom-set C(A, B) is a commutative monoid; and • distributes over composition.
Proof The addition is associative due to the following diagram commutes. The neutral element of C(A, B) is 0 A,B since the following commutes: hence C is enriched over commutative monoids. To see that the addition distributes over composition recall the identities Proposition 40 In a category with biproducts the injections and projections shown in Eq (1.5) satisfy Proof For any product A × B we have π 1 × π 2 • ∆ = π 1 , π 2 = 1 A×B and dually for any coproduct ∇ • in 1 + in 2 = 1 A+B . Hence Due to the universal property of the biproduct, the canonical map from A ⊕ B to itself is equal to 1 A⊕B . Therefore The binary biproduct may be generalised to arbitrary finite families of objects A 1 , . . . , A n by iteration. Upto an associativity isomorphism, the n-fold biproduct is characterised by the diagram Arrows between biproducts have matrix representations as described at the start of this section, and composition of of arrows gives the usual matrix multiplication.
Proposition 41 Suppose we have arrows The second equation follows directly from the naturality of the diagonal and codiagonal maps.
Proposition 39 implies that any category with biproducts is enriched over CMon, the category of commutative monoids; conversely, we have the following. Given a category C we can construct the free biproduct structure on C, first by freely enriching C over CMon and then taking matrices over the resulting category.
Proposition 46 Let C N be the category whose objects are those of C and where C N (A, B) = N(C (A, B)), the free commutative monoid on C(A, B). Then C N is CMon enriched and the inclusion of C into C N is a universal arrow from C to a CMon-category.
Proposition 47 Let C be a CMon-category and let Matr(C) be the category whose objects are n-tuples of objects of C, for n ≥ 1, and whose arrows are matrices of arrows C. Then Matr(C) is semi-additive, and the evident semi-additive embedding of C into Matr(C) is universal among semi-additive functors from C to semi-additive categories.

Compact Closed Categories with Biproducts
Proposition 48 Let C be a monoidal closed category with biproducts; then there are natural distribution isomorphisms Proof Since A ⊗ − is a left adjoint it preserves colimits and hence the diagram Corollary 49 In a monoidal closed category C with biproducts, the functor A ⊗ − : C → C is additive.
In fact we can easily construct the distribution isomorphisms explicitly. Let Then If a compact closed category C has a binary product − × − then the duality (·) * sends every product diagram to a coproduct diagram As mentioned earlier, if C has a terminal object 1 then 1 * is initial. Hence the question of whether or not C has biproducts boils down to whether the canonical maps are isomorphisms. It turns out that this is always the case.

Proposition 50 (Houston) If a compact closed category C has all finite products (or coproducts) it has all finite biproducts.
Proof See Houston [Hou08].

Corollary 51 In any compact closed category with biproducts:
• we have natural isomorphisms • the duality (·) * is an additive functor.
It then follows that we may choose the biproduct in any compact closed category so that the equation holds for all objects A.
We now turn our attention to the construction of the free compact closed category with biproducts upon some polycategory P. The earlier results of Propositions 46 and 47 described how to freely construct the biproduct as matrices whose elements are drawn from some category C, and this will provide the core of our proof.
Write CBP to denote the free compact closed category with biproducts generated by a compact polycategory P. We refer to the objects of P, their images under (·) * , and the constants 0 and I as the literals of CBP. According to Corollary 51, in any compact closed category with biproducts, (·) * commutes with ⊕, and since both the biproduct and tensor structures are freely generated, the objects of CBP are formed from the literals by repeated application of the functors (− ⊗ −) and (− ⊕ −) †. Any object may therefore be described by such a functor and a vector of literals.
Lemma 52 Let G be a functor constructed from (− ⊗ −) and (− ⊕ −); then G is naturally isomorphic to a normal functor N G Proof The required isomorphism is constructed from the distributivity isomorphisms.
Hence we have that all arrows in CBP have the form ? and since f ′ is an arrow between normal functors, it has matrix elements for a more general treatment of this.
each of which is a (possibly empty) sum of arrows from the freely constructed compact structure, Circ(P).
Hence the free compact closed category with biproducts is produced by forming Matr(Circ(P) N )-that is, the free biproduct category on top of the free compact closed category-and simply adjoining the distributivity isomorphisms.
This free construction is the final piece of category theory needed in this article. In Section 1.4 we'll introduce a system of proof-nets that represent this category.

Tensor-Sum Logic
In this section we will introduce the syntax of tensor-sum logic in a sequent calculus LTS, and give it a semantics over a suitable category. Let A be a category and denote by F A the free compact closed category with biproducts generated by A. The atomic formulae of LTS will be the objects of A, and the arrows of A will give its non-logical axioms. In the next section we will generalise to the situation where the generators are a polycategory, but that requires a proof-net presentation. For now we stick to this simpler case, since the essence of the connectives can be seen equally well via a sequent presentation.
Definition 53 The formulae of LTS are given by the following grammar: where A ∈ Obj A are called atoms. Given a formula F we define its de Morgan dual F * by: We use the convention that letters A,B,C etc, range over the atoms, while X,Y ,Z etc, range over arbitrary formulae. We take for granted that all formulae are in de Morgan normal form-that is, with the negation symbol (·) * occurring only on atoms.

Definition 54 A sequent of LTS has the form
where Γ and ∆ are lists of formula, respectively called the antecedent and succedent of the sequent, and L is a tree whose leaves are labelled by loops from A. Given two such trees L 1 , L 2 , we write L 1 · L 2 for the tree formed by fusing their roots; we write L 1 + L 2 for the tree whose root has L 1 and L 2 as its only subtrees. We don't distinguish between a loop l in A and the tree whose only leaf node is l.

Definition 55 An LTS proof is a tree of inferences drawn from the rules shown in Figure 1.2; the leaves of the tree must be drawn from the axiom group. A proof is called multiplicative if (1) only multiplicative formulae occur in it; and, (2) no rule from the additive group occurs. The reduced sequent calculus consisting only of multiplicative proofs we call LT.
One could summarise the rules of LTS as "multiplicative-additive linear logic with self-dual connectives". Certainly one can embed MALL into LTS by translating both multiplicative connectives as ⊗ and both additives as ⊕ and nothing will go terribly wrong. However, since both connectives of LTS are self-dual, many cuts which would be forbidden in MALL are allowed in LTS, and we must introduce some novel rules to deal with this. It is worthwhile to point out some of the more idiosyncratic rules.
Axiom Rule In the case that A is a discrete category then the only arrows are identities so we regain the usual A ⊢ A axioms. The restriction of axioms to ground types is for technical convenience; identity axioms for every type are constructable, and indeed admissible.
Unit Rule An distinctive feature of compact closed categories is the presence of loops, so incorporating this rule allows an exact connection between the syntax and the semantics to be established. Perhaps more importantly, the unit rule allows "circular" cuts to be eliminated.
Cut Rule The cut rule, as shown here, might be better described as a trace rule. The more traditional cut rule, The Cut: Multiplicative Group: σ, τ permutations.

Fig. 1.2. Inference Rules for LTS
can be defined in LTS using the mix and exchange rules, viz: Mix Rule The mix rule (combined with the two rules for tensor) asserts that the comma is the same on both sides of the sequent, unlike The Cut: Multiplicative Group: σ, τ permutations.
Additive Group: where i = 1 or 2. Fig. 1.3. Semantics for rules of LTS most logics. It allows usual two-premise cut and tensor rules to be constructed.
Zero Rule Without the zero rule certain cuts are impossible to remove. It has been noted that the logic of biproducts is inconsistent: every sequent is provable. By including the zero axiom we embrace this inconsistency. A more computational point of view is that every type is inhabited, at least by the divergent program, or in the quantum setting, the evolution with zero probability.
Sum Rule This rule asserts that each LTS proof is a (finite) formal weighted sum of LTS proofs, with the weights given by the pair L and L ′ . Otherwise this rule performs a similar role to the mix, allowing the usual binary rules for additives to be constructed. The formulae of LTS are just the objects of A hence we shall not even bother to distinguish them notationally. To give semantics for LTS its remains to translate proofs into arrows of F A.
Definition 56 Let π be an LTS proof of the sequent We define its denotation, an arrow π : X 1 ⊗ · · · ⊗ X n → Y 1 ⊗ · · · ⊗ Y m by recursion over the structure of π according to the rules shown in figure 1.3.
Theorem 57 (Cut Elimination) For every LTS proof π of the sequent Γ ⊢ ∆; L there exists a proof π ′ of Γ ⊢ ∆; L which contains no occurrence of the cut rule, and such that π = π ′ .
The proof proceeds in the standard way so we omit it here. (The general strategy can be translated from the proof-net version presented below.) We remark that preserving the denotation is the non-trivial part; otherwise the zero rule can be used to give a cut-free proof immediately.
We would like the formulae of LTS to be in exact correspondence with the objects of the free category F A. Unfortunately we have several equations between syntactically distinct formulae. To work around this blemish we will introduce a special class of formulae.
Definition 58 A formula is called multiplicatively reduced if it is different to I and contains neither X ⊗ I nor I ⊗ X as a subformula, for any formula X. A sequent is monoidally reduced if all its formula are monoidally reduced.
A formula is called additively reduced if it has no subformula of the forms 0 ⊕ X, X ⊕ 0, 0 ⊗ X or X ⊗ 0. A sequent is additively reduced if all its formulae are.
A formula or sequent which is both multiplicatively and additively reduced is simply called reduced.
The content of this definition is that the only place that I may occur in a reduced formula is under the ⊕ connective; the only reduced formula containing 0 is 0 itself.
Proposition 59 Every sequent is provably equivalent to a reduced one.
Proof We have the following provable equivalences: This result means that the reduced formulae of LTS are in 1-1 correspondence with the objects of F A. We call a proof reduced if its conclusion is reduced. Note that we cannot restrict to reduced formulae throughout, since they must be introduced to construct certain formulae, for example I ⊕ I. Having dealt with the objects of F A we turn out attention to the arrows.
Theorem 60 (Completeness) Let f be an arrow in F A; there exists a cut-free LTS proof π such that f = π .
We again omit the proof since it follows from a more general result proved below. However this theorem marks the end of the line as far as the sequent system is concerned. Our attempt to find a proof-theoretic characterisation of F A founders on the usual curse of sequent calculi: the existence of distinct cut-free forms for the same proof. LTS is especially bad in this respect since it enjoys a great many sound commuting conversions.

Generalised Proof-Nets
In this section we define a system of two-sided proof-nets constructed over the generators of a compact symmetric polycategory P. The resulting system of proof-nets will be denoted PN(P). Using these proof-nets we obtain a logical system closer in behaviour to a term system: every proof-net has a unique normal form. The availability of such normal forms allows us to make an exact correspondence between the PN(P) and the free compact closed category with biproducts.

Tensor-Sum Proof-Nets
Graphical notations for monoidal categories have been studied as far back as the early seventies [Kel72, Pen71, JS91] and such 2-dimensional representations provide for beautifully simple reasoning in a setting normally awash with coherence equations. When proofs are represented graphically, as in proof-nets for multiplicative linear logic, a further advantage is gained: by relaxing the allowed shapes of proofs, from trees to graphs, the artificial sequentiality imposed by the use of sequent proofs is removed. Work on MLL [Gir87b, DR89, BCST96] extended the graphical tensor notation to the case of two tensors which enjoy a "weak" distribution law † [CS97]. In these settings the two tensors are essentially similar, and indeed can be made formally dual. In the following we study the case a single self-dual tensor so while much of the work of [BCST96] applies, we can make some significant simplifications, and are forced into some complications too, but the we retain a purely graphical language for the multiplicative fragment of LTS, closely related to the diagrams of [Coe05b]. We note that because LTS is so permissive, no correctness criterion,à la Danos and Regnier [DR89], is needed here.
However, into our multiplicative paradise we must admit the additive connectives and this complicates matters. We handle the additive structure using a system of slices and boxes. The notion of slices in linear proof-nets first appeared in Girard's original [Gir87a] but was not entirely satisfactory for the unrestricted multiplicative-additive fragment of linear logic; the correctness of the proof-structure as a whole could not be derived from the correctness of its slices [Gir96]. A similar notion was later employed in [HvG03] to give a satisfactory notion of MALL proofnet. In the more restricted setting of polarised linear logic, the naive use of slices works very well since the additional constraint of polarity forces the additive connectives to cohere nicely [LTdF04].
Just as compact closed categories are degenerate models of the multiplicative part of linear logic, the biproduct is a degenerate version of the linear logic's additive connectives. Happily, this degeneracy means that slicing will give good results, for essentially the opposite reasons to the polarised case: we have so many equations that the question of correctness becomes trivial. Slices and boxes are defined by mutual recursion.

Premise: No incoming edges; one outgoing edge. The edge is labelled
with an arbitrary formula and the link is unlabelled. Conclusion: One incoming edge; no outgoing edges. The edge is labelled with an arbitrary formula and the link is unlabelled. Unit: No incoming edges; two outgoing edges. The first outgoing edge is labelled X * , the other, X, for some formula X. The link itself is labelled by η. Counit: Two incoming edges; no outgoing edges. Each counit is labelled by ǫ and its incoming edges are labelled by X and X * for an arbitrary formula X. Tensor: Two incoming edges labelled X and Y ; one outgoing edge labelled X ⊗ Y .
Cotensor: One incoming edge labelled X ⊗ Y ; two outgoing edges labelled X and Y .

Circle: No incoming or outgoing edges; a circle is a closed loop labelled by a formula.
Axiom: Each polyarrow f : A i i → B j j in Arr P defines a link labelled by f . Its n incoming edges are labelled by A 1 , . . . , A n and its m outgoing edges are labelled by B 1 , . . . , B m . Plus 1: One incoming edge labelled X; one outgoing edge labelled X ⊕ Y , for an arbitrary formula Y . A proof-slice is oriented such that edges enter the node from the top, and exit from the bottom. This implies that any premise, star or unit link is above the links they are connected to and, conversely, any conclusion, costar, or counit links are below the links they are connected to.
The order of premises and conclusions is significant, and the type of a proof-slice is the pair (Γ, ∆) of lists of formulae determined by the premises and conclusions respectively. Usually this will be written as a sequent Γ ⊢ ∆. The empty slice is valid slice, with type ⊢ .
A premise or conclusion link is called atomic if the formula labelling it is a literal; a proof-slice is called atomic if all its premises and conclusions are atomic. A slice is called flat if it contains no boxes Proof-slices are permitted to be disconnected or cyclic, when considered as directed or undirected graphs. In particular, an edge may leave a link and return as an input to the same link, although the labelling on edges will prohibit this for all except axiom links. If a proof-slice is directed-acyclic then it is called process-like. A box may be empty; in which case it may have any inputs and outputs. Indeed, such an empty box is the only normal proof of the formula 0.
Operationally a box may be viewed as local classical knowledge (or rather, non-determinism) embedded in one part of the system -the distribution of addition over composition codes the transmission of this information. The details of this distribution, presumably mediated by some classical control structure, will not investigated here, but it seems an interesting direction for further exploration.
Definition 63 Let s be a proof-slice; define its depth d(s) as where the b i range over the boxes occurring in s. Let b be a box containing slices {s i } i ; then define its depth d(b) by

Definition 64 A PN(P) proof-net is a PN(P) box of finite depth.
According to Definition 64 every slice is contained in a box, which is called the ambient box for that slice. Also, if a slice s contains a box, the slices contained within that box are not considered part of s; that is, from the point of view of their containing slice boxes are considered totally opaque. On the other hand, the phrase "a slice in proof-net π" should be understood unrestrictedly, as denoting a slice at any level of nesting with the proof-net structure. Since proof-nets have finite depth, any box occurring within a proof-net is itself a valid proof-net; hence there is no loss in generality by assuming that ambient box is always the top-level.
Since PN(P) proof-nets are rather unwieldy objects, it is helpful to introduce a symbolic shorthand for working with them algebraically. Writing s i for a sequence of slices, a box containing those slices is written as a summation, i s i . The crucial ingredient is a "slice with a hole". A hole can be thought of as a link with arbitrary incoming and outgoing edges; we write s{ } to represent a slice with a hole. Such an object is not a valid part of our notation, we introduce it only in order write such expressions as s{t}, where t is a proof-net fragment having the same incoming and outgoing edges as the hole in s such that the slice produced by replacing the hole in s with the fragment t is a valid slice. Simply writing the empty brackets { } denotes a slice which all hole -it has no structure besides its type. We use letters π, π ′ to denote proofnets; π{ } should be understood as a proof-net with a hole in one of its slices. When we write π{ }{ } to denote a proof-net with two holes, it should always be understood that both holes are in the same slice. It will never be necessary to speak of holes in separate slices.
Example 65 This 2 sliced net encodes the distribution of ⊗ over ⊕.
Since categories are a special case of polycategories, we can define PN(A) equally well when A is just a category. In this case the axiom links have exactly one input and one output; there is one for each arrow of A. In this situation we can translate from LTS sequent proofs to proof-nets.
Definition 66 (Translation from sequents) Given an LTS proof π, we define a proof-net N π by recursion over the structure of π.
• If proof π is just an f -axiom, let N π be the single slice containing just the corresponding axiom link, connected to a premise and a conclusion link, leaving a net of type A ⊢ B. • If proof π is a just an application of the h-unit rule for some h : A → A, we form N π by introducing h as an axiom, as described above, and forming a cut between, as described below, between its input and output. • If π is simply an application of the zero rule then N π is an empty box with the desired type. • If π arises from π ′ by an application of the cut rule for arrow on some formula X form N π from N π ′ by replacing, in every slice of N π ′ , the premise link corresponding to the negative occurrence of X with an η X link, and replacing the conclusion link corresponding to the positive occurrence of X with an ǫ X link. The X * output of the new unit link is connected to the X * input of the new counit link. • Suppose π arises from subproofs π 1 and π 2 by the mix rule. Then let N π = {N π 1 }{N π 2 } i.e a single slice containing two boxes, one for each subproof. • If π arises from π ′ by an application of the (⊗-R) rule, form N π adding, in every slice, a tensor-link between the conclusions of N π ′ corresponding to the active formulae of the rule. • If π arises from π ′ by an application of the (⊗-L) rule, form N π adding, in every slice, a cotensor-link between the premises of N π ′ corresponding to the active formulae of the rule. • If π arises from π ′ by an application of the (*-R) rule on some formula X, form N π adding, in every slice, an η X -link between to the premise of N π ′ corresponding to the active formulae of and connect its X * output to a new conclusion link. • If π arises from π ′ by an application of the (*-L) rule on some formula X, form N π adding, in every slice, an ǫ X -link between to the conclusion of N π ′ corresponding to the active formulae of and connect its X * output to a new premise link. • If π arises from π ′ by an application of the (I-R) rule, form N π adding, in every slice, a star-link, connected a new conclusion link.
• If π arises from π ′ by an application of the (I-L) rule, form N π adding, in every slice, a costar-link, connected a new premise link. • If π arises from π ′ by an application of the (⊕ i -R) rule, form N π by adding a plus-i-link to the conclusion corresponding to the active formula in every slice of N π ′ . • If π arises from π ′ by an application of the (⊕ i -L) rule, form N π by adding a coplus-i-link to the premise corresponding to the active formula in every slice of N π ′ . • Suppose π arises via an application of the sum rule to proofs π 1 and π 2 ; suppose also that N π 1 = i s i and N π 2 = j t j . Then let N π = i s i + j t j .

Normalisation
Definition 67 Let e be an edge in a slice, going from some link L 1 to link L 2 . We say that e is expandable when: (i) e is labelled by a a compound formula (i.e. either X⊗Y or X⊕Y ); (ii) L 1 is a premise, cotensor, or coplus link; and, (iii) L 2 is a conclusion, tensor, or plus link.
Definition 68 (Rewrite Steps) Let ν, µ be proof-nets; define a one step reduction relation on proof-nets R β such that ν R β µ if ν can be rewritten to µ by one of the following local rewrite rules.

Circle reversal:
where A is an atom.
Expansion Rules ⊗and ⊕-expansions: An edge from link L 1 to link L 2 and labelled by a compound formula X is expanded when both of the following hold: • L 1 is a cotensor coplus, or premise link; and • L 2 is a tensor plus, or conclusion link.

Unboxing Rule
If a slice s contains a box b = i t i , replace s in the ambient box via i.e. make a new copy of s for each slice in b, and in each replace b with the slice.
Definition 69 Let β be the transitive, reflexive closure of R β and let = β be the symmetric closure of β -.

Proof No rewrites change the premises or conclusions, hence the type is unchanged by β-reduction.
We now begin the approach the proof that β-reduction is strongly normalising. First some intermediary definitions.
Definition 71 Let X be a formula; define its depth d(X) by Lemma 72 Let e be an expandable edge labelled by X; then e can be expanded to give a box with at most d(X) slices.
Proof We use induction on X. Suppose that X contains a connective; the expansion rule for that connective will introduce expandable edges labelled by the subformulae Y and Z. By induction, these yield boxes with d(Y ) and d(Z) slices respectively. If X = Y ⊗Z; then the expansion rule introduces the new edges in parallel; applying the unboxing rule to one then the other we, obtain d(Y )d(Z) slices.
Alternatively suppose X = Y ⊕ Z. The expansion rule introduces a box containing two slice, with an expandable edge in each. Again, we can apply the unboxing rule twice, and obtain a box with d(Y ) + d(Z) slices.

Definition 73
We define the size of a proof-net π, written n(π) by mutual recursion over slices and boxes. Let s be a slice with boxes b i ; then where N s is the number of links found in s, except conclusions, premises and boxes. If we have a box b = j t j then let Definition 74 We define the rank of a proof-net π, written r(π) by mutual recursion over slices and boxes. Let s be a slice with boxes b i ; then where K s is the total number of times the symbols ⊗ and ⊕ occur in the labels of expandable edges of s. If we have a box b = j t j then let The following lemma is immediate from the definitions: Lemma 75 Let s{ i t i } be a slice in a proof-net; then the following hold: Theorem 76 (Termination) Every β-reduction sequence is finite.
Theorem 77 (Local Confluence) If a proof-net π β-reduces to π 1 and π 2 by different rewrites r 1 , r 2 , then there exist sequences of rewrites s 1 , s 2 such that Proof Within a box, rewrites on one slice do not affect any of the other slices. Hence, for a conflict to exist, either r 1 and r 2 both affect the same slice or that r 2 operates on a child slice of that where r 1 acts. Otherwise there is no conflict between the rewrites and they can be trivially unified.
The rules also exhibit locality in the vertical direction. The only rule which allows slices on different levels to interact is the unboxing ruleand this only pulls slices up from the level below. Hence if r 1 and r 2 act on slices which are more than two levels apart they do not conflict.
Observe that there are three kinds of rules in the system: those that add slices to the ambient box (just the unboxing rule); those that delete a slice (the zero rule and the incoherent case of ⊕-elimination); and those which have purely local effect (all the rest). We'll deal with the cases in that order.
Suppose that the rewrite r 1 is the unboxing rule; without loss of generality we have Since we need only consider the case where r 2 acts on s{ } or one of the t j , the other slices s i will be neglected. Suppose r 2 acts on s{ }: • If r 2 is the unboxing rule acting on some other box then we have which can be unified by repeating r 2 in each slice on the left, and r 1 in each slice on the right: • If r 2 deletes s then this must be due some structure in s{ } hence the same rule can delete each of the s{t i }, which suffices to unify the divergence, • If r 2 is any other rewrite then we have where r 2 matches some structure in s{ }, hence it is still available in each of the s{t i }, permitting the unification: Now suppose r s acts on one of the t i , which we simply call t.
• Suppose r 2 is the unboxing rule acting on some box in t: Then we have the divergence which we unify using repeated application of the unboxing rule.
• Suppose that r 2 deletes t; then same rule will delete s{t}, which will unify the divergence. • Otherwise r 2 rewrites t to some t ′ ; again this same rewrite will do s{t} → s{t ′ } which will unify the divergence.
This shows that the unboxing rule cannot conflict with the others. Now suppose that r 1 deletes slice s. This implies that s contains either a pair of incoherent ⊕-links or an edge labelled by 0. Notice that none of the slice-local rules can remove either of these features from the graph. Hence regardless of which rule it is, no slice-local rule r 2 can block r 1 , so the divergence can always be unified by deleting s. Of course, If r 2 also deletes s then there is no divergence.
Finally we consider the case where both r 1 an r 2 are slice-local. Since all the action is within a single slice, it suffices to show that any pair of overlapping rewrites which diverge can be unified.
Due to the large number of expansion rules, there are a very large number of potential critical pairs. Fortunately the rules are very regular and have been carefully designed to ensure their confluence. For reasons of space we do not include this analysis here, but checking all the pairs is a routine, albeit lengthy, exercise.
All divergent rewrites can be unified, hence PN(P) is locally confluent under β-reduction.
Proof Since β-reduction is confluent, each proof-net has a unique normal form; since it is terminating, every rewrite sequence must arrive at the normal form.
Having established the existence of β-normal proof-nets, we now characterise them intrinsically. Recall that for multiplicative linear logic proof nets [Gir87b], the structure of a cut free proof can be separated into the axiom structure and the connective structure. The following lemmas give a similar result, flattening the additive structure and pushing the connectives to the outside of the proof-net.
Lemma 79 Let π be a normal proof-net; then every slice of π is flat.
Proof If any slice contains a box, we can apply the unboxing rule, contradicting the normality of π.
Since the box structure of a normal net is trivial, we turn our attention to the structure of the slices. Notice that we will assume that a normal slice is in a normal net, and hence the rule for 0-elimination has been applied, implying that a normal slice contains no edge labelled by 0.
Lemma 80 Let π be a normal proof-slice, and suppose x is a link in π.
• If x is a tensor or a plus link, all links below x are tensors, pluses, or conclusions.
• If x is a cotensor or coplus link, all links above x are cotensors, copluses, or premises.
Proof Let x be either a tensor link, or a plus link. Its outgoing edge is labelled by some formula, either X ⊗ Y or X ⊕ Y ; suppose there is a link below it, called x ′ . Note that since π is normal, x ′ cannot be a box.
• If x ′ is a counit then it is labelled by a non-atomic formula, hence an ǫ-expansion rewrite applies and π is not normal. • If x ′ is an axiom, it has an incoming edge labelled by a non-atomic formula, which contradicts the definition of axiom link.
Now there are two cases depending on what kind of link x is.
• Suppose that x is a tensor link; then x ′ cannot be a coplus link because its incoming formula is X ⊗ Y . Suppose that x ′ is a cotensor link: then rewrite rule ⊗-elim applies, hence π is not normal. • Suppose that x is a plus link; then x ′ cannot be a cotensor link because its incoming formula is X ⊕Y . Suppose that x ′ is a coplus link: then rewrite rule ⊕-elim applies, hence π is not normal.
Hence x ′ cannot be a coplus, cotensor, counit, or axiom link. If it is a conclusion then the hypothesis is satisfied. If x ′ is a tensor or plus link, then by induction all the links below x ′ are also tensors, pluses, or conclusions. The case when x is a cotensor or coplus is exactly dual.
Corollary 81 Any normal proof-slice π can be formed from a normal atomic slice π ′ by adding tensor and plus links to its conclusions and cotensors and copluses to its premises.
Corollary 82 All the edges of a normal atomic proof-net are labelled by literals.
Proposition 83 An atomic proof-slice is normal if and only if: all its edges are labelled by atomic formulae; its circles are labelled by positive atoms; no edge is labelled by 0; every edge labelled by I connects a premise to a costar, or a star to conclusion; and no unit link is connected to a counit link; Proof If π is normal, Corollary 82 gives that all its edges' labels are atomic; by its normality no unit is connected to a counit since otherwise rewrite ηǫ-elim 1 or 2 would apply. Since π is normal, it contains no boxes, hence the formula 0 can only introduced by a premise of conclusion link, but which in this case the 0 elimination rule would apply.
Since π is atomic, the formula I may only be introduced by star, costar, premise, or conclusion links; any such edge labelled by I is can be eliminated unless it connects a premise to a costar, or a star to conclusion as required.
Conversely, suppose that π is atomic, such that all the above conditions are satisfied. Since all its edges are labelled by literals, none of the expansion rules can apply. For the same reason it contains no tensor, cotensor, plus, coplus, or box links, hence rewrites for ⊗, ⊕, 0, and circle elimination do not apply, nor does unboxing. Star and costar links can only appear in forms such that the I elimination rules do not apply. By hypothesis, no unit is connected to a counit, hence rewrites ηǫ-elim 1 and 2 cannot apply, and circles are labelled by positive literals the circle reversal rule does not apply. Since, no rewrites are possible, π is in its normal form.

The categorical structure of PN(P)
In this section we prove main remaining theorems about PN(P). First we show that PN(P) forms a compact closed category with biproducts; and then we show that it is a representation of the free compact closed category with biproducts generated by P.

Proposition 84
The class of proof-nets, PN(P), forms a category.
The objects of PN(P) are LTS formulae. An arrow π : X → Y is a proof-net whose only premise is X and whose only conclusion is Y . Two arrows in PN(P) are considered equal if they have the same normal form.
Note that the restriction to single formulae is rather weak since the comma of tensor-sum logic is implicitly the tensor; given a proof-net not in this form, we may insert tensor links between the conclusions, and cotensors between the premises, to obtain a proof-net of the desired kind. The restriction to single formulae also avoids having to provide a bracketing, since the connectives of LTS are not strictly associative.
We define the identity proof-net 1 X to be a net with one slice, containing only a premise link and a conclusion link, both labelled by X. (Note that since the edge linking them may be expandable, this is not usually the normal form.) Before defining composition of nets, we first define it for slices. Suppose s, t are proof-slices such that both the conclusion of s, and the premise of t, are some formula X; we define t • s by removing the con-clusion link of s, removing the premise link of t, and forming a new slice by joining the two graphs along the resulting open edges. Notice that this operation is manifestly associative. Further, we have equations since, considering the first case only, we have simply removed a conclusion link from s and adjoined an identical conclusion link. The other case is the same. Now let f : X → Y and g : Y → Z be proof-nets, with slices f i and g j respectively; their composition g • f = ij g j • f i where the composition on slices is as above. Given a third net h : Z → W , we have so composition of proof-nets is associative as required. The identity equations follow directly from the slice case. Hence all the axioms required to be a category are satisfied.

Proposition 85 PN(P) is compact closed.
First we define the monoidal structure of PN(P). Let f : X 1 → Y 1 and g : X 2 → Y 2 be proof-nets; then define their tensor product as unit and counit maps η X and ǫ X are defined by the nets Proof This property follows directly from the slice structure of proofnets. If f, g : X → Y are proof nets then f + g is just the proof net containing all slices of both f and g; since the order of the slices is not significant this operation is commutative. The net with no slices, denoted ∅, gives the zero element.
Proof Obviously, the formula 0 is the zero object. Note that for any formula X, the empty proof-net (i.e the net with no slices) provides a proof ∅ : X → 0 and also ∅ : 0 → X.
Suppose that we have a proof-net f : X → 0. Each slice in f must contain a conclusion link labelled by 0; hence by the rule for 0-elimination, every slice of f must be deleted, so the normal form of f is the empty proof-net. Hence, for every X, there is exactly one arrow of type X → 0, and similarly there is exactly one arrow 0 → X, so 0 is both initial and terminal in PN(P).

Proposition 88 PN(P) has biproducts.
Proof Consider the following one-sliced proof-nets: Observe that the rules for ⊕-eliminations imply that Next, consider the identity map 1 X1⊕X2 . We have the equation via the rewrite sequence below. -- Since we can form these maps for any pair of objects and, by Propositions 86 and 87, PN(P) is a CMon-category with a 0 object, the result now follows by Proposition 42.

Proposition 89
In PN(P) we have natural distribution isomorphisms: Proof The required maps are given by the proof-nets show below. We leave the reader to check that these nets do indeed define natural isomorphisms.
The preceding six propositions established that PN(P) is indeed a compact closed category with biproducts as described in Section 1.2.8. Note further that the objects of PN(P)-the LTS formulae-are freely generated from the atoms, which are themselves the objects the underlying polycategory P. Every object of PN(P) is therefore isomorphic to a formula in disjunctive normal form, where the X ji are literals, and the constants 0 and I occur only when a sum or product is empty. (We assume some given bracketing of the connectives.) Hence every proof-net f : X → Y is equivalent to some f ′ of the form: Since f ′ is a arrow between sums, we can consider its matrix elements π i • f ′ • in j . Without loss of generality take f ′ to be in normal form; by Lemmas 79 and 80 f ′ consists of flat slices, whose connective links are all at the outside, and since its type is in disjunctive normal form all its plus and coplus links are outside all its tensor and cotensor links. Hence where each f k is a proof-slice between multiplicative formulae. Hence, where k ′ ∈ {k | j k = j and i k = i}. By Corollary 81 each of the f k ′ corresponds to a unique normal atomic slice, which is monoidally reduced. Hence, the only part the structure of PN(P) which is not freely generated by its connectives are the normal atomic slices; we now characterise these, and by so doing prove that PN(P) is a representation of the free compact closed category with biproducts generated by P.
The reduced normal atomic proof-slices are very closely related to the P-labellable circuits. Let PN(P) N denote the subcategory of PN(P) determined by the multiplicative formulae, and flat, single-sliced proofnets. We take PN(P) N to be monoidally strict, hence its arrows are in 1-1 correspondence to the reduced atomic proof-slices. A simple formal transformation produces a circuit from each such proof-slice, and viceversa. This correspondence can be boosted upto a pair of functors Circ(P) Lemma 90 Suppose ν is an atomic normal proof-net; suppose e is an edge in ν labelled by a negative literal. One of the following holds: • e connects a premise to a conclusion; • e connects a premise to a counit link; • e connects a unit link to a conclusion.  Proof By Lemma 80, ν contains no tensor, cotensor, plus, or coplus links, nor any boxes; neither axioms nor stars nor costars can introduce negative negative edges, therefore e must connect either a premise, unit, counit or conclusion. Since the proof-net is normal, e cannot join a unit to a counit by the preceding lemma. Since an edge cannot be incoming or outgoing at both endpoints the pairings unit/unit, counit/counit, premise/premise, conclusion/conclusion, conclusion/counit and premise /unit are excluded. This leaves the three possibilities claimed. These can occur validly in a normal proof-net as shown by Fig. 1.6.
Suppose that π : Γ → ∆ is normal and atomic; then π can be rewritten to produce an P-labelled circuit c(π) : Γ → ∆ by the following procedure.
(i) The premises and conclusions of π become the boundary nodes of c(π); the premises form dom c(π) and the conclusions cod c(π). They are labelled by the edges formulae and signed according to whether the atom is positive or negative.
(ii) For all edges e labelled by a negative literal A * , reverse e's direction, and change its labelling to A. This guarantees that negatively signed nodes in the codomain have incoming edges, and vice versa. (iii) Erase every unit and counit node, merging their incident edges, which are now pointing in the same direction. (iv) The remaining links of π must all be axioms links. These become the internal nodes of c(π). At each node x, the ordering on in(x) and out(x) is simply that of the components of the domain and codomain of the arrow (in A) which labels that node.
Lemma 90 guarantees that c(n) really is a circuit. There is a dual procedure, taking a circuit f : i A i → j B j to a normal atomic proof-net.
(i) The nodes in dom f become premises; those of cod f , conclusions. (ii) If e is an edge, labelled by A, going from some node n to a premise p, replace e with a counit-link whose incoming edges are from e and p, labelled by A and A * respectively. (iii) If e is an edge, labelled by B, going to some node n from a conclusion c, replace e with a unit-link whose outgoing edges go to e and c and are labelled by B and B * respectively. (iv) The interior nodes of f become axiom links, each determined by the label on the corresponding node.
This defines a proof-net p(f ) : A 1 , . . . , A n ⊢ B 1 , . . . B m , which by Proposition 83 is normal. The two procedures are mutually inverse, which leads to the following characterisation result.
Definition 91 Let X be formula; an additive path for X is a map which assigns a boolean value to each occurrence of ⊕ in X.
Given an additive path b we can define a purely multiplicative formula X (b) by replacing each subformula Y ⊕ Z with Y if b assigns 0 to this ⊕ and Z if b assigns 1.
Theorem 92 Let π be a normal proof-slice; then π is completely determined by its type, an additive path for its domain and codomain, and a P-labellable circuit.
⊗ -⊗ ⊗ --· · · · · · · · · · · · · · · · · · · · · · · · -⊗ ⊗ ⊗ --· · · · · · premise type Γ Fixed by the conclusion type ∆ Fixed by the Defines a unique P-labelled circuit f Proof Suppose that π has type X ⊢ Y . Given a formula X, and an additive path b, let X, b be the list of literals produced by replacing every occurrence of ⊗ in X (b) by a comma. By Lemma 80, π can be decomposed into three layers: on top π X,b of type X ⊢ X, b consisting only of cotensor, coplus, and costar links; the middle π − : X ⊢ X, b ⊢ Y, b ′ which is both normal, reduced, and atomic; and at the bottom π Y,b ′ : Y, b ′ ⊢ Y consisting only of tensors, pluses and stars. The layers π Γ and π ∆ are uniquely determined by X, b and Y, b ′ , while π − is uniquely determined by the circuit c(π − ).
Corollary 93 A normal reduced atomic slice is completely determined by a P-labelled circuit f.
Justified by the corollary we write π ∼ f for any normal reduced atomic slice π. The required functors F and U are now easily defined.
For each A of PN(P), let U A be the positively signed singleton, labelled by A; then define U (A * ) = (U A) * and U (X ⊗ Y ) = U X ⊗ U Y . Let π β To map Circ(P) into PN(P), let f be a circuit; then let F f be the proof-net obtained from p(f ) by adding tensor links to all the conclusions (bracketed to the left) and, similarly, cotensors to all the premises.
Proof Obviously, from the construction of U and F , we have U F = Id. On the other hand, a proof-net π : X → Y only differs from F U π : F U X → F U Y by the associativity of the tensor, hence Id ∼ = F U .
This theorem establishes that the matrix elements of a proof-net π in PN(P) are nothing more than formal sums of circuits over P; i.e. element of the free compact closed category generated by P. Hence we have the main result: Theorem 95 The category of proof-nets PN(P) is the free compact closed category with biproducts generated by the compact symmetric polycategory P.

Conclusions
To recap: we sketched how key parts of quantum mechanics can be formalised in the language of compact closed categories and biproducts; we demonstrated how to represent quantum processes as proof-nets, and showed that normalisation of such proof-nets allows some of the behaviour of the corresponding processes to be simulated.
We introduced the formal syntax of tensor-sum logic, and its proofnet notation. We showed that proof-nets are strongly normalising, and characterised the normal forms. Finally we proved the main theorem: that the category of proof-nets is exactly the free compact closed category with biproducts generated by the polycategory from which its axioms are drawn. This result can be viewed as a coherence theorem for compact closed categories with biproducts, in the style of Kelly and Laplaza's classic result for compact closed categories [KL80].
To return to our starting point, tensor-sum logic is almost an orthogonal theory to Birkhoff-von Neumann quantum logic. Tensor-sum logic is entirely preoccupied with the areas that quantum logic neglects: compoundness, interaction, and control. However, as the main theorem shows, we abdicate all responsibility for the internal structure of our quantum systems. Since our arrows are characterised by normal proofnets, they are nothing more than type constructors wrapped around the generators: the fine structure must be described by an equational theory of the generators. We can view this as a strength: the logic is extremely general and could be easily applied to situations other than quantum computing. On the other hand, we suffer strong limitations on how much of quantum mechanics can be formulated in this setting without adjoining ad hoc rules to account for the particular situations we are modelling.
In a sense, this work is the end of the road for those "logical" approaches to quantum mechanics deriving from linear logic †. Already the dividing line substructural logic and algebra is thin, and what we have shown here is that, while proof-theoretic tools may suffice for the coarse business of putting together systems and pulling them apart again, the true quantum structure is living in the (poly)category of generators, and more subtle algebraic tools are needed to tease out the details. In particular the importance of spectra in quantum mechanics weighs against any approach based on natural transformations. Recent work [CPV08, CPP08, CD08] provides a categorical account of observables which is essentially algebraic. Fittingly, such theories have graphical representations which allow them to slot into the proof-net framework as generators. In that case combining the two systems would yield a well behaved two-level system of types and terms suitable for representing quantum processes under classical control.