Nicolas Brunner

Marc Kaplan

Anthony Leverrier

Paul Skrzypczyk

Dimension of physical systems, information processing, and thermodynamics

published or not. The documents may come

We investigate the problem of giving a model independent definition of the dimension of physical systems. We give two definitions of dimension, based on measurements and on the capacity of storing information. While both definitions coincide in classical and quantum mechanics, they are in general different in generalized probabilistic theories. We discuss in detail the case of a theory known as 'boxworld', and show that such a theory features systems with a dimension mismatch. This dimension mismatch can be made arbitrarily large by using an amplification procedure. Furthermore, we show that the dimension mismatch of this model has strong consequences on its power for performing information-theoretic tasks, leading to the collapse of communication complexity and to the violation of information causality. Finally, we discuss the consequences of a dimension mismatch from the perspective of thermodynamics, and ask whether this effect could break Landauer's erasure principle and thus the second law.

Any theory aimed at explaining and predicting experimental observations makes use of a concept of dimension, which represents the number of degrees of freedom considered in the model. Loosely speaking, the dimension of a system corresponds to the number of perfectly distinguishable (or orthogonal) configurations the system can be prepared in. For instance a classical coin can be prepared in two orthogonal states, heads or tails, and has thus dimension two. A qubit, i.e. a quantum coin, also has dimension two. By performing any possible measurement, one can distinguish between two orthogonal qubit states, but no measurement can perfectly distinguish between three different qubit states. More generally, the dimension of a quantum system is given by the notion of the Hilbert space dimension.

The dimension of a physical system (classical or quantum) also characterizes the amount of classical information that can be encoded in the system and subsequently retrieved. Notably, classical and quantum systems of the same dimension d can carry the same amount of classical information, namely log 2 d bits of information [1]. However, it is not the case that a classical system of dimension d can always be substituted for a quantum system of the same dimension d. In fact, reproducing the behaviour of the simplest quantum system, the qubit, requires classical systems of infinite dimension [2] (see also [3]). This shows that quantum theory is much more economical in terms of dimension compared to classical physics. Reproducing (even approximatively) the statistics of simple quantum experiments involving systems of low Hilbert space dimension requires the use of classical systems of higher dimensions [4]. The reason for this is that classical and quantum states, even of the same dimension, are fundamentally different objects. On the one hand, for a classical system, the dimension d always corresponds to the number of pure states the system can be prepared in. For finite dimension d, there are d pure states. On the other hand, a quantum system, say a qubit, can be prepared in infinitely many different pure states, and two real numbers (hence infinitely many classical bits) are necessary to characterize a pure state. Indeed this difference has a strong impact on the capabilities of each theory for information processing.

The above shows that comparing classical and quantum physics from the point of view of dimension gives an interesting perspective on quantum mechanics, first as a physical theory but also on its power for information processing. More generally, one may ask how quantum mechanics compares to other physical theories, such as generalized probabilistic theories (GPTs) [5], a general class of theories featuring quantum and classical mechanics as special cases. In fact, understanding what features identify quantum mechanics among GPTs is a deep question, which may lead to a reformulation of quantum theory based on more physical axioms, see e.g. [5][6][START_REF] Dakic | Deep Beauty: Understanding the Quantum World through Mathematical Innovation[END_REF][START_REF] Masanes | [END_REF][9][START_REF] Masanes | Proc. Nat. Acad. U.S.A[END_REF]. Discussing information processing and physical properties of GPTs may give insight to this question [5,[START_REF] Janotta | [END_REF][12][13][14].

However, comparing different physical theories from the point of view of dimension is in general not a trivial issue. This is due to the fact that each theory has its own notion of dimension, usually based on the structure of the theory itself-e.g. in quan-tum mechanics, dimension is associated to the Hilbert space, the basic structure supporting quantum states and measurements. But one may ask if there exists a universal, model independent definition of dimension that could be used to compare different models.

Here, we explore the problem of defining the dimension of physical systems independently of the underlying model. At the back of our mind is the question of whether quantum mechanics is special as far as dimension is concerned.

We start by discussing two definitions of dimension which we believe are natural. First we consider a notion of dimension related to the measurements that can be performed on a system. Our second notion of dimension refers to the amount of information that is potentially extractable from the system. While these two notions of dimension happen to coincide in classical and quantum physics, they are nevertheless different in general. We show that this is the case in a specific GPT known as 'boxworld' [5]. We say that such a model features a dimension mismatch.

Moreover, we shall see that the dimension mismatch of boxworld appears to be directly related to its astonishing information-theoretic power. So far this information-theoretic power was only discussed in the context of spatially separated systems, that is considering communication tasks assisted by nonlocal (but no-signaling) correlations, see e.g. [16][17][18][19][20][21][22][23][24][25][26][27][28][29][30][31][32]. In particular, it was shown that the existence of maximally nonlocal correlations (so-called Popescu-Rohrlich (PR) boxes [15]) would lead to the collapse communication complexity [16], and to the violation of the principle of information causality [22]. Here we recover these results but following a different approach. Considering only single systems, we show that both the collapse of communication complexity and the violation of information causality, are direct consequences of the dimension mismatch of boxworld.

Finally we discuss the consequences of a dimension mismatch from a more physical perspective, related to thermodynamics. Specifically, we explore these ideas in the context of Maxwell's demon and Landauer's erasure principle [33][34][35], and raise the question of whether theories with a dimension mismatch would break the second law of thermodynamics.

I. TWO DEFINITIONS OF DIMENSION

Measurement dimension, which we denote here d m , is defined as the number of outcomes of an ideal nondegenerate measurement. By an ideal measurement, or pure measurement, we refer to a measurement that is perfectly repeatable, i.e. when obtaining one particular outcome, repeating the measurement will always lead to the same outcome. By non-degenerate, we mean that the measurement is not coarse grained. In quantum mechanics, ideal non-degenerate measurements are rank-one projective measurements.

Equivalently, measurement dimension can be viewed as the number of orthogonal pure states of the system, i.e. that can be perfectly distinguished in a single measurement. Hence there is a set of states {ω 1 , . . . , ω d m } and a measurement with d m outcomes, such that outcome i has probability one for state ω i . This implies that d m bits of information can be encoded in the system and subsequently retrieved via a measurement.

The second definition, information dimension, which we denote d i , is the number of states of the system that are perfectly distinguishable pairwise. More formally, d i is the largest integer such that there exists a set of states {ω 1 , ..., ω d i } such that for any pair ω i , ω j with 1 ≤ i < j ≤ d i , there is a measurement that perfectly distinguishes ω i from ω j . Note that these measurements can be different for all pairs of states, and can be chosen to be binary without loss of generality. In other words, information dimension characterizes the maximal number of states which are pairwise orthogonal.

Finally, note that the measurement dimension is always smaller than or equal to the information dimension. Indeed, if a system can be prepared in d m different states which can be perfectly distinguished in a single measurement, then each pair of states in this set is also perfectly distinguishable by this measurement, hence d m ≤ d i . Below we shall see that in quantum mechanics equality holds, i.e. d m = d i , while there exist more general theories where this is not the case, that is where d m < d i .

II. MEASUREMENT AND INFORMATION DIMENSIONS COINCIDE IN CLASSICAL AND QUANTUM MECHANICS

We start with the case of quantum theory. Consider a quantum system, the states of which are given by vectors in a Hilbert space of dimension d, i.e. C d . Then, any orthonormal basis consists of d pure states. One can always define an observable acting on C d , formed by the d states of an orthonormal basis. Thus, we get that d m = d, that is the measurement dimension is equal to the Hilbert space dimension.

It is also straightforward to see that the information dimension is equal to the Hilbert space dimension. Consider a set of d quantum states which are perfectly distinguishable pairwise. These states are pairwise orthogonal and thus form an orthonormal basis in C d , hence we get that d i = d.

We conclude that for quantum systems, measurement dimension and information dimension coincide. Indeed, this is also the case for classical systems. A classical system of dimension d features d pure states, which are all pairwise distinguishable. On the other hand, a collection of classical states which are all pairwise distinguishable, can all be distinguished by a single measurement.

III. DIMENSION MISMATCH IN GENERALIZED PROBABILISTIC THEORIES

While it may come to no surprise that measurement dimension and information dimension coincide in quantum mechanics, we shall see that this is not necessarily the case in generalized probabilistic theories. When measurement dimension and information dimension differ, i.e. when d m < d i , we say that the theory features a dimension mismatch. Before discussing this aspect, we give a brief review of the concepts of GPTs; for more details, we refer the reader to Refs [5,[START_REF] Janotta | [END_REF]14,36].

A. Basic concepts

The state of a system is an abstract object that defines the outcome probabilities for all the measurements that can be performed on a system. The state space Ω is the set of states that a system can be prepared in. Linearity is an essential feature of GPTs, which ensures that Ω is convex and can be represented by a vector space. Pure states are extremal points of Ω. Other states are called mixed, as they can be decomposed as a convex mixture of pure states. More generally, linearity is important as it ensures that the model is no-signaling, i.e. that it does not allow for instantaneous transmission of information, hence avoiding a direct conflict with relativity.

Consider now measurement outcomes, usually termed effects. These are a maps from Ω to the interval [0, 1], hence assigning a probability to each state of Ω. Here, linearity implies that effects are affine maps. A measurement is then given by a set of effects {e i } such that ∑ i e i = u, where u is called the unit effect, i.e. the effect assigning value 1 to every state in Ω. This condition ensures that all states are normalized. Similarly to quantum theory, a measurement is given by a decomposition of the unit effect (the identity), ensuring that the probabilities for each outcome sum to one. The set of effects, Ω * , is taken to be the convex hull of extremal effects and the unit effect.

Let us now discuss our above notions of dimension in the context of GPTs. We focus here on a specific GPT known as boxworld [5], studied later in e.g. [37][38][39]. An interesting aspect of this model is that it features nonlocal correlations (i.e. leading to violation of Bell inequalities); in fact, boxworld features all possible no-signaling correlations, such as the PR box. We start by discussing the simplest system in boxworld. This is a single physical system on which two possible binary measurements can be performed. Such a system is usually represented as a "black box" with two possible inputs (or measurements), denoted x = 0, 1, and two possible outputs (or measurement outcomes), denoted a = 0, 1 (see Fig. 1a). The pure states of this system are those for which the outcome a is a deterministic function of the input x, that is

a = αx ⊕ β (1)
where α, β = 0, 1. There are thus four pure states.

Using the vectorial representation of GPTs, the state space Ω of this simple system can be conveniently represented by a 2D cube [54], i.e. a square (see Fig. 1b).

The vertices of the square represents the four pure states ω j with j = 1, ..., 4. All other states are convex mixtures of the pure states, and are thus mixed states. The set of effects Ω * , given by the dual of the state space, is also a 2D cube, but rotated compared to the state space (see Fig. 1c). Pure (or extremal) effects correspond the four possible measurement outcomes, i.e. inputing x in the box and getting outcome a. For more details on this system, in particular on its state space, we refer the reader to Refs [5,[START_REF] Janotta | [END_REF]. Clearly, our system features only two ideal measurements, which correspond to input x = 0 or x = 1 in the box. Both measurements have two outcomes, hence we have that measurement dimension is d m = 2. This system can be used to transmit exactly one bit of information, and thus can be considered as a generalization of the qubit-in fact it is often referred to as a g-bit, i.e. generalized bit [5]. Moreover, such a system can be considered as the reduced local part of a PR box.

On the other hand, we see immediately that the information dimension is d i = 4, since any pair of pure states can be perfectly distinguished by performing either the x = 0 or x = 1 measurement. Hence we see that our g-bit system features a dimension mismatch, as d i > d m .

FIG. 1: The simplest system in boxworld. (a) This system can be understood as a black box taking a binary input x = 0, 1 and returning a binary output a = 0, 1. The state of the system is described by a conditional probability distribution P(a|x). (b) The state space Ω of the system can be represented as a square in R 2 . The system thus features four pure states, ω j . For each pure state, the outcome a is a deterministic function of the input x, as indicated. At the centre of Ω is the maximally mixed state, that is, where a is independent of x and random. (c) The space of effects, Ω * , is the dual of Ω. It features four extremal effects, e j , which correspond to the four measurement outcomes, i.e. obtaining output a for a given input x. The probability of e j on any state is easily determined. For instance, effect e 1 has probability one for states ω 1,2 and probability zero for states ω 3,4 . There are two pure measurements for this system: the first is composed of effects e 1 and e 3 , hence corresponding to input x = 0; the second is composed of effects e 2 and e 4 , hence corresponding to input x = 1. Note that e 1 + e 3 = e 2 + e 4 = u, where u is the unit effect.

B. Amplification of dimension mismatch

While the g-bit has a dimension mismatch of a factor 2, we will see now that there exist in boxworld systems with an arbitrarily large dimension mismatch. Such systems, which are a straightforward generalization of the g-bit, can in fact be constructed by composing g-bits. Hence, dimension mismatch can be amplified.

We presented the g-bit system as a black box featuring two possible (pure) binary measurements x = 0, 1, with outcome a = 0, 1. Consider now a black box with D possible binary measurements x = 0, . . . , D -1, with outcome a = 0, 1. Following the g-bit construction, the state space of our system is now a hypercube in R D . The system features 2 D pure states. Each state associates a deterministic outcome (a = 0 or a = 1) to each of the D possible measurements. In the state space, each pure state corresponds to one of the vertices of the D-dimensional hypercube.

The measurement dimension is d m = 2 for all D, since all pure measurements are binary. Hence, the system can be viewed as a generalization of a bit, since only one bit of information can be retrieved by performing a measurement on it. From now on, we will thus refer to this system as a hypercube bit [START_REF]Note that the hypercube bits discussed here are different objects than the 'hyperbits[END_REF].

On the other hand, any pair of pure states of the hypercube bit can be perfectly distinguished, since there is (at least) one measurement x for which two different pure states give different outcomes. Therefore, the information dimension is d i = 2 D . Hence, as D increases, we obtain an arbitrarily large dimension mis-match.

Finally, we present a procedure to construct hypercube bits by composing g-bits. To define the composition of systems in a GPT, one has to choose a tensor product. In boxworld, one uses the 'maximal tensor product' [5] (see also [START_REF] Janotta | [END_REF]). Intuitively, this means the following: a bipartite (or more generally multipartite) system is considered as a valid state, if (i) it does not allow for instantaneous transmission of information (i.e. it is no-signaling) and (ii) upon performing a measurement on one system, and for each outcome of this measurement, the other system is prepared (or steered) into a state that is valid (i.e. inside the initial state space) [56].

Consider the composition of two g-bits. The resulting system can be represented as a black box shared between two observers, such that each observer can perform one out of two possible measurements with binary outcomes. We denote x i the measurement of observer i and a i its outcome. The state space obtained by taking the maximal tensor product of two g-bits has been extensively discussed [40]. For our purpose, it is convenient to express the pure states of this bipartite state space according to their correlations:

a 1 ⊕ a 2 = αx 1 x 2 ⊕ βx 1 ⊕ γx 2 ⊕ δ (2)
where α, β, γ, δ = 0, 1. We thus obtain 16 pure states [57], which can be divided into two classes: (i) 8 local deterministic states, for which α = 0, and (ii) 8 nonlocal PR boxes, for which α = 1. Note that states in class (i) can be obtained by taking two copies of a g-bit: hence a i = f (x i ). On the contrary, states in class (ii) feature nonlocal correlations (e.g. of the form a 1 ⊕ a 2 = x 1 x 2 ) which achieve maximal violation of the Clauser-Horne-Shimony-Holt Bell inequality. To ensure no-signaling, such states have full local randomness, that is p(a i = 0|x i ) = 1/2. At this point, our composed system has d m = 4. To obtain a hypercube bit, we project it onto a subspace. More precisely, we apply the projection (a 1 , a 2 ) → a = a 1 ⊕ a 2 . This is analogous to parity projections in quantum theory. The resulting system has measurement dimension d m = 2 and information dimension d i = 16, and is in fact isomorphic to a hypercube bit with D = 4.

The above procedure can be applied starting from the composition of k g-bits, hence resulting in a system that is isomorphic to a hypercube of dimension D = 2 k . Specifically, one considers all pure states in the maximal tensor product of k g-bits with correlations of the form a 1 ⊕ a 2 ⊕ ... ⊕ a k = f (x 1 , ..., x k ) where f is an arbitrary deterministic boolean function of k bits-note that in general there exist additional pure states which are not of this form [41]. Hence we obtain 2 2 k pure states. After performing the projection (a 1 , ..., a k ) → a = a 1 ⊕ a 2 ⊕ ... ⊕ a k we get a state space that is isomorphic to the hypercube of dimension 2 k . Therefore, when composing g-bits using the maximal tensor product (in other words assuming only no-signaling), we obtain systems with an arbitrarily large dimension mismatch.

Finally, note that the possibility of amplifying dimension mismatch depends on the way systems are composed, i.e. which tensor product is chosen. Since the choice of tensor product will affect the strength of nonlocal correlations featured in the model, there appears to be a direct relation between the possibility of amplifying dimension mismatch and the strength of nonlocal correlations. This aspect will be discussed in more detail in Section V.

IV. DIMENSION MISMATCH AND COMMUNICATION POWER

In this section, we investigate the consequences for information processing of the dimension mismatch of hypercube bits. We consider information-theoretic tasks using protocols with 'one-way communication'. Specifically, we consider the situation in which Alice can prepare a hypercube bit in any desired state, encoding certain information in it. Then she sends the system to Bob, via an adequate (non-classical) channel. Bob finally performs a measurement on the received hypercube bit, which allows him to extract part of the information that Alice encoded in the system.

We shall see that the dimension mismatch of hypercube bits enhances their communication power compared to classical and quantum resources, leading to maximal violation of information causality and to the collapse of communication complexity. In fact, these enhancements in communication power are captured by the fact that hypercube bits are tailored for computing the index function, which we discuss first.

A. Index function

Consider the following communication complexity problem. Alice receives a uniformly sampled bit string of length n, {b i } i=1...n . Bob receives a random index k = 1, ..., n. The goal for Bob is to output the value of the bit b k . This problem is known as computing the index function. Its classical and quantum communication complexity is n bits [START_REF] Nayak | Proceedings of 40th IEEE FOCS[END_REF]. Hence, using classical or quantum systems for the index function requires systems of dimension increasing exponentially with n. Below we show that a hypercube bit of dimension D = n allows for computing the index function on inputs of length n. Since we have here that d m = 2 independently of n, this is in stark contrast with classical and quantum resources.

After receiving her input bit string {b i } i=1...n , Alice prepares a hypercube system of dimension D = n in a pure state {ζ i } i=1...D such that ζ i = b i . This means that the outcome of measurement x i is ζ i = b i (for i = 1, ..., D) . Then she sends the system to Bob. Upon receiving index k, Bob performs measurement x k and obtains outcome ζ k . He thus retrieves correctly the bit value b k .

Note that the ability to compute the index function depends only on the information dimension d i , but is independent of the measurement dimension d m . For hypercube bits, the index function can be computed for arbitrary n (taking D = n). Nevertheless, the measurement dimension remains fixed, d m = 2, meaning that the system is binary, in the sense that only one bit of information can be retrieved by performing a measurement on it. This is thus in stark contrast with systems featuring no dimension mismatch, such as classical and quantum systems.

B. Information causality

The principle of information causality [22] was initially formulated in a scenario where classical communication is assisted with pre-shared non-local correlations. The principle limits the strength of nonlocal correlations by restricting the power of classical commu-nication assisted by nonlocal correlations. In certain cases, information causality allows one to recover the boundary between quantum and super-quantum correlations [22,23].

Here we consider a variant of information causality, in a scenario with one-way communication. Alice encodes information in a physical system (for instance a hypercube bit) and sends it to Bob, who retrieves information by performing a measurement on the system. In this context, the principle should limit Bob's conditional gain of information depending on the information capacity of the physical system that is sent. Consider Alice receiving a bit string of length n, {b i } i=1...n , and Bob receiving an index k = 1, ..., n and asked to give a guess β for the value of bit b y . Then information causality can be written as

n ∑ j=1 I(b j : β|k = j) ≤ H(d m ), (3)
where d m is the measurement dimension of the system and H(d m ) is its capacity, that is the amount of bits of information that be retrieved from the system by performing a measurement on it. Indeed, this task is essentially identical to the index problem discussed above. Hence by using a hypercube bit of dimension D = n, Alice and Bob can achieve ∑ n j=1 I(b j : β|k = j) = n > 1 = H(d m ) and violate maximally information causality. In other words, one can implement a perfect 1-out-of-n random access code [START_REF] Nayak | Proceedings of 40th IEEE FOCS[END_REF] using a hypercube bit of dimension D = n.

Note that a related formulation of information causality for single systems was recently considered in an axiomatic reformulation of quantum theory [START_REF] Masanes | Proc. Nat. Acad. U.S.A[END_REF].

C. Collapse of communication complexity

The collapse of communication is arguably the strongest demonstration of the communication power of PR boxes [17,19]. Initially proved for pure PR boxes [16], the result was later extended to classes of noisy PR boxes [18,21]. While these works considered classical communication assisted with pre-shared nonlocal resources, we consider here the case where Alice prepares a physical system and sends it to Bob.

Consider a boolean function f : X × Y → {0, 1}, where X denotes the set of possible bit strings b = {b i } i=1...n received by Alice, and Y the set of bit strings c = {c j } j=1...m for Bob. The goal is that Bob should output the value of the function f (b, c), for any possible inputs. The communication complexity of the function is then the amount of information that needs to be communicated from Alice to Bob in order for Bob to compute the function. Classically, this represents the number of bits C required by the most economical protocol, hence this protocol uses classical systems of dimension d = 2 C . Using quantum resources, the communication complexity is the number of qubits Q necessary to compute the function, hence the optimal protocol requires quantum systems of Hilbert space dimension d = 2 Q . More generally, we see that a protocol using a system of measurement dimension d m has communication complexity C = log 2 (d m ), as this represents the amount of information that is extracted from the system by Bob's measurement.

By adapting the index protocol discussed above, any boolean function can be computed by having Alice sending a single hypercube bit to Bob. The protocol is as follows. Suppose Alice and Bob want to compute a given function f . Upon receiving her input bit string b, Alice computes locally the value of the function f (b, c) for all possible input bit strings c of Bob. Next, she prepares a hypercube bit of dimension D = |Y| = m (i.e. the number of possible inputs y for Bob) in the state {ζ i } i=1,...,D such that

ζ i = f (b, c = i).
Hence, we need a hypercube bit of sufficiently large dimension, such that D = m. Bob, upon receiving his bit string c, performs the corresponding measurement and accesses the bit ζ c , hence the value of the function f (b, c).

Since the above protocol uses a single hypercube bit, it has trivial communication complexity C = 1, independently of the size of the input bit strings. Indeed, this is in stark contrast with the case of classical or quantum resources, for which there exist functions whose communication complexity is not trivial, that is, C is an increasing and unbounded function of the size of the problem [START_REF] Cleve | Quantum Computing and Quantum Communication[END_REF].

D. Steering

We just showed that the existence of hypercube bits would lead to the violation of information causality and to the collapse communication complexity. Hence we recover previously known results about the dramatic enhancement of communication power observed in boxworld compared to quantum theory [16,22]. However we followed a different approach. While previous works considered the power of classical communication assisted by the strong nonlocal correlations (i.e. PR boxes) available in boxworld, we studied here the power of hypercube bits for information-theoretic tasks, considering protocols in which Alice prepares a hypercube bit and then sends it to Bob, who finally performs a measurement on it.

It turns out however that both approaches can be connected, as the communication of a hypercube bit is essentially equivalent to the communication of one classical bit assisted with PR boxes, as we shall see below.

To see this, consider first the case in which Alice prepares a hypercube bit of dimension D in a state {ζ i } i=1,...,D and sends it to Bob who recovers bit b k by performing measurement k. This protocol can be simulated by D PR boxes, shared between Alice and Bob, and one bit of classical communication from Alice to Bob. We denote the inputs (outputs) of PR box number i by x i (a i ) for Alice and y i (b i ) for Bob. First, Alice enters bit ζ i in PR box number i for i = 1, ..., D. She then sends to Bob the bit c = a 1 ⊕ ... ⊕ a D . Bob, who wants to retrieve bit k, inputs y k = 1 and y j = 0 for

j = k. Finally, Bob outputs c ⊕ b 1 ⊕ ... ⊕ b D = ζ k .
Consider now the converse problem. We want to simulate a situation where Alice and Bob share n PR boxes, Alice sends one bit of classical communication to Bob who then extracts one bit of information f (b, c) which depends on the inputs b and c they received. It is sufficient here to consider a deterministic function f . Upon receiving her input b, Alice computes locally f (b, c) for all possible inputs of Bob c = 1, ..., m. She then prepares a hypercube bit of dimension D = m in a state {ζ i } i=1,...,D , such that

ζ i = f (b, c = i).
Upon receiving the hypercube bit from Alice, Bob performs measurements to retrieve the bit ζ c , and retrieves the desired bit f (b, c), as he would have in the situation they wanted to simulate.

Thus, we conclude that the communication of a hypercube bit can be replaced by a single bit of classical communication assisted by a sufficient number of PR boxes, and vice versa. The fact that the hypercube bit has measurement dimension d m = 2 corresponds to the fact that a single bit of classical communication is sufficient in the above protocol. Also, the information dimension d i is related to the number of required PR boxes in the protocol we gave above.

V. DISCUSSION

We have discussed the problem of characterizing the dimension of physical systems in a model independent way. We introduced two definitions for the dimension which we believe are rather natural. One is related to the number of outcomes of a pure measurement and the other to the number of pairwise perfectly distinguishable states. These two notions of dimension coincide in quantum mechanics and are equal to the Hilbert space dimension, the usual (but model-dependent) measure of dimensionality of quantum systems. We showed that this is not the case in certain generalized models, such as boxworld. Hence these models feature a dimension mismatch, in the sense that the number of states which are pairwise perfectly distinguishable exceeds the number of outcomes of a pure non-degenerate measurement. Moreover, we described a procedure to amplify the dimension mismatch, leading to an arbitrary large mismatch. We then investigated the link between dimension mismatch and communication power, showing violation of information causality and the collapse of communication complexity in boxworld.

An interesting point is that we recover here previous results on the astonishing communication power in boxworld, but using a different approach. Instead of considering two observers sharing pre-established nonlocal correlations and sending classical communication to each other, we considered the case in which one observer sends a physical system (a hypercube bit) to the other. Hence it is the properties of a single system which are exploited here, instead of the strong nonlocal correlations of bipartite systems. This illustrates the strong connection that exists between the properties of the state space of a single system with the strength of nonlocal correlations that are obtained when looking at bipartite systems [START_REF] Janotta | [END_REF]26,27,44]. It is important to note that, although we do not directly consider bipartite (or multipartite) systems, we did make an assumption about how single systems can be combined. Specifically, in the procedure we used to amplify dimension mismatch, it was essential to assume that systems can be combined using the maximal tensor product, which does ensure the existence of maximally nonlocal correlations, such as PR boxes. This shows that dimension and nonlocality are connected.

Another aspect worth mentioning is that concepts of dimension discussed here allow us to characterize information processing in GPTs without introducing a notion of entropy, a notoriously problematic issue [45][46][47].

It would be interesting to see how general the present results are. Considering an arbitrary model featuring a dimension mismatch, can this dimension mismatch always be amplified? What are the information-theoretic properties of such a model? For instance, does a dimension mismatch always lead to a collapse of communication complexity? Another possible direction is to consider the present ideas for the problem of deriving quantum theory from a set of physically reasonable axioms [5][6][START_REF] Dakic | Deep Beauty: Understanding the Quantum World through Mathematical Innovation[END_REF][START_REF] Masanes | [END_REF][START_REF] Masanes | Proc. Nat. Acad. U.S.A[END_REF]. Indeed, imposing that measurement dimension and information dimension are equal seems to have nontrivial consequences on the structure of the underlying physical theory and its information-theoretic capabilities. Note also that a recent work considered a concept of dimension equivalent to our notion of information dimension in order to motivate the use of the Hilbert space in quantum theory [48].

Another direction would be to see whether the present approach is related to the principle of local orthogonality [30,31] and the exclusivity principle [32]. The main idea behind both principles is to demand the following. Consider a set of events, of the form (a 1 ...a n |x 1 ...x n ), such that all possible pairs of events are orthogonal (i.e. exclusive), then the sum of the probabilities of each event should not exceed one. That is, events which are pairwise orthogonal are all mutually exclusive. Indeed, the notion of pairwise orthogonality that appears here is reminiscent of our definition of the information dimension, which represents the maximal number of states which are all pairwise orthogonal. We conjecture that, in a model without dimension mismatch, that is where d m = d i = d, the principle of local orthogonality should be satisfied. Consider a set of d pairwise orthogonal events, i.e. measurement outcomes or effects. Then one should be able to construct from these effects a d-outcome measurement, which is pure and non-degenerate. Indeed, such a measurement must be properly normalized, i.e. the sum of the probabilities of each outcome must be one. Hence, if such a measurement can always be constructed, it follows that local orthogonality is satisfied. It would be interesting to derive a formal proof from the above intuitive argument. The converse link also deserves attention, that is, does local orthogonality imply no dimension mismatch, i.e. d m = d i = d? Note that an interesting step in this direction was recently given in Ref. [50], where it is shown that the set of 'almost quantum correlations' [49] (i.e. a superset of quantum correlations which is proven to satisfy local orthogonality and that does not allow for trivial communication complexity) will have no dimension mismatch.

VI. THERMODYNAMICS PERSPECTIVE

Finally, we believe that the present ideas also have implications from a more physical perspective, in particular for thermodynamics. The main point we would like to raise here is that a dimension mismatch may potentially lead to a violation of the second law. We formalize this question by asking if a system with a dimension mismatch, such as the hypercube bit, could lead to the realization of Maxwell's demon.

We first argue that the concept of measurement dimension is related to the cost of erasing the information encoded in a physical system. For instance, in quantum theory, the cost of erasing a qudit (a system in a Hilbert space of dimension d and a vanishing Hamiltonian) is given by k B T log(d) (see e.g. [35]), where T is the temperature of the external bath used to perform the erasure, and k B is the Boltzman constant. This can be done by performing an ideal and nondegenerate measurement on the system and then erasing the information about the outcome of this measurement, which costs exactly k B T log(d). Note that the state of the system after the measurement is one of the d pure eigenstates of the measurement. Hence, one can finally reset the system back to any desired pure state by applying a suitable unitary transformation to the system-this operation being unitary does not change the entropy of the system, and since the Hamiltonian vanishes it costs no energy.

Following this line of reasoning, we will now argue that the cost of erasing a hypercube bit is k B T log d m = k B T log 2. An aspect that deserves clarification here is how one should define the post-measurement state in the case of a hypercube bit. For simplicity, let us focus on the g-bit. We assume here that the postmeasurement state for measurement x = 0 is given by the pure state ω 1 when a = 0, and ω 3 when a = 1. Similarly for measurement x = 1, we assume that the post-measurement state is ω 2 when a = 0, and ω 4 when a = 1. Indeed, this choice is somehow arbitrary, and it would be possible to define the postmeasurement states differently. Nevertheless, our choice is a valid one, and is consistent with the model, to the best of our knowledge. Note also that when performing one measurement, say x = 0, the information about the other measurement outcome, x = 1, is erased, ensuring that only one bit of information can be retrieved by performing a measurement on the gbit.

Now let us investigate the cost of erasing a g-bit. Similarly to the quantum case, one first performs a measurement, say x = 0. Then the g-bit will be found in state ω 1 or ω 4 (depending on the outcome of the measurement) and can then be reset to any desired pure state by applying a suitable rotation of the square (equivalent to a unitary operation). Finally, the information about the measurement outcome must be erased, which costs k B T log (2). Generalizing this procedure to hypercube bits, one thus gets that the cost of erasure of a hypercube bit is k B T log d m = k log 2.

Next, one may wonder what is the significance of the information dimension in this context. It is tempting to conjecture that the information dimension captures the amount of information that the system can store, i.e its memory size. Consider Maxwell's original thought experiment, in which a demon separates fast and slow particles, hence making heat flow from a cold bath into a hot one-for more details, see [34,35]. For each incoming particle, the demon, after determining the speed of the particle, decides to let it cross the partition or not. The demon must then store this information in his memory. Now let us imagine that the demon's memory is in fact a hypercube bit of dimension D. We denote its state {ζ i } i=1,...,D . Say the hypercube bit is initially in the state (ζ 1 = 0, ζ 2 = 0, ..., ζ D = 0). After deciding on the fate of the first incoming particle, the demon stores the information in the hypercube bit: if he decided to let the particle pass (0), the demon leaves the state of the hypercube unchanged; but if he decides to bounce the particle back (1), he rotates the hypercube bit to the state (ζ 1 = 1, ζ 2 = 0, ..., ζ D = 0), that is he flips the first bit of the state. The demon then proceeds similarly for the next D -1 incoming particles, by updating the state of the hypercube such that the bit of information created in the k-th run is stored in ζ k .

It thus seems that the demon can store D bits of information in the hypercube bit. After that, in order to continue sorting the particles, the demon must erase the hypercube bit, and make sure to reset it to the initial state (ζ 1 = 0, ζ 2 = 0, ..., ζ D = 0). According to Landauer's erasure principle [33], this operation should cost him at least k B T log(D). However, we have seen above that the cost of erasing a hypercube bit (and resetting it to an arbitrary pure state) is in fact much smaller, namely k B T log d m = k B T log 2. Hence we get a contradiction with Landauer's principle, thus implying a violation of the second law.

At this point it is legitimate however to question the significance of the information dimension here. In particular, one may argue that, since only one bit of information can be retrieved from the hypercube bit, the memory size of such a system is in fact 2, and not D as argued above. However, one is forced to ad-mit that all the information about which particles the demon let pass and which ones he did not let pass is encoded in the hypercube bit, and that any single bit of this information can be retrieved at any moment. Moreover, for each new bit of information to be stored, the system is either left in the same state (if the bit to be stored has value 0) or flipped to an orthogonal state (if the bit value to be stored is 1). Another aspect that one may question, is our choice of post-measurement states. In fact, one may argue that the above argument gives evidence that such a choice of post-measurement state is not a valid one. However that would imply postulating the validity of the second law (rather than deriving it), which is not desirable. An interesting question would be to revisit the above argument with other choices of post-measurement states, for instance choosing postmeasurement states to be mixed ones. Could one then find a rule for choosing post-measurement states such that the second law would be satisfied in the above protocol?

While we are not in position to make a final claim at this moment, we nevertheless believe that these ideas reveal an intriguing aspect of generalized systems such as the hypercube bit. We hope that the above discussion will stimulate further work on thermodynamics in GPTs (see also work in [51][START_REF] Barrett | talk at the conference 'Fundamentals of Physics and Information[END_REF][START_REF] Hänggi | [END_REF] for different approaches), which we feel may have impact on our understanding of quantum theory.

Acknowledgements. N.B. acknowledges financial support from the Swiss National Science Foundation (grant PP00P2 138917) and the EU DIQIP. M.K. acknowledges financial support from ANR retour des post-doctorants NLQCC (ANR-12-PDOC-0022-01). PS acknowledges support by the Marie Curie CO-FUND action through the ICFOnest program.


Richard F Blute

Alessio Guglielmi

Ivan T Ivanov

Prakash Panangaden

Lutz Straßburger

A logical basis for quantum evolution and entanglement

We reconsider discrete quantum causal dynamics where quantum systems are viewed as discrete structures, namely directed acyclic graphs. In such a graph, events are considered as vertices and edges depict propagation between events. Evolution is described as happening between a special family of spacelike slices, which were referred to as locative slices. Such slices are not so large as to result in acausal influences, but large enough to capture nonlocal correlations. In our logical interpretation, edges are assigned logical formulas in a special logical system, called BV, an instance of a deep inference system. We demonstrate that BV, with its mix of commutative and noncommutative connectives, is precisely the right logic for such analysis. We show that the commutative tensor encodes (possible) entanglement, and the noncommutative seq encodes causal precedence. With this interpretation, the locative slices are precisely the derivable strings of formulas. Several new technical results about BV are developed as part of this analysis.

Introduction

The subject of this paper is the analysis of the evolution of quantum systems. Such systems may be protocols such as quantum teleportation [START_REF] Nielsen | Quantum Computation and Quantum Information[END_REF]. But we have a more general notion of system in mind. Of course the key to the success of the teleportation protocol is the possibility of entanglement of particles. Our analysis will provide a syntactic way of describing and analyzing such entanglements, and their evolution in time.

This subject started with the idea that since the monoidal structure of the category of Hilbert spaces, i.e. the tensor product, provides a basis for understanding entanglement, the more general theory of monoidal categories could provide a more abstract and general setting. The idea of using general monoidal categories in place of the specific category of Hilbert spaces can be found in a number of sources, most notably [START_REF] Abramsky | A categorical semantics of quantum protocols[END_REF], where it is shown that the notion of a symmetric compact closed dagger monoidal category is the correct level of abstraction to encode and prove the correctness of protocols. Subsequent work in this area can be found in [START_REF] Abramsky | Physics from computer science[END_REF], and the references therein.

A natural step in this program is to use the logic underlying monoidal categories as a syntactic framework for analyzing such quantum systems. But more than that is possible. While a logic does come with a syntax, it also has a builtin notion of dynamics, given by the cut-elimination procedure. In intuitionistic logic, the syntax is given by simply-typed λ-calculus, and dynamics is then given by β-reduction [START_REF] Lambek | Introduction to Higher-order Categorical Logic[END_REF]. In linear logic, the syntax for specifying proofs is given by proof nets [START_REF] Girard | Linear logic: Its syntax and semantics[END_REF]. Cut-elimination takes the form of a local graph rewriting system.

In [START_REF] Blute | Discrete quantum causal dynamics[END_REF], it is shown that causal evolution in a discrete system can be modelled using monoidal categories. The details are given in the next section, but one begins with a directed, acyclic graph, called a causal graph. The nodes of the graph represent events, while the edges represent flow of particles between events. The dynamics is represented by assigning to each edge an object in a monoidal category and each vertex a morphism with domain the tensor of the incoming edges and codomain the tensor of the outgoing edges. Evolution is described as happening between a special family of spacelike slices, which were referred to as locative slices. Locative slices differ from the maximal slices of Markopolou [START_REF] Markopoulou | Quantum causal histories[END_REF]. Locative slices are not so large as to result in acausal influences, but large enough to capture nonlocal correlations.

In a longer unpublished version of [START_REF] Blute | Discrete quantum causal dynamics[END_REF], see [START_REF] Blute | Discrete quantum causal dynamics[END_REF], a first logical interpretation of this semantics is given. We assign to each edge a (linear) logical formula, typically an atomic formula. Then a vertex is assigned a sequent, saying that the conjunction (linear tensor) of the incoming edges entails the disjunction (linear par) of the outgoing edges. One uses logical deduction via the cut-rule to model the evolution of the system. There are several advantages to this logical approach. Having two connectives, as opposed to the single tensor, allows for more subtle encoding. We can use the linear par to indicate that two particles are (potentially) entangled, while linear tensor indicates two unentangled particles. Application of the cut-rule is a purely local phenomenon, so this logical approach seems to capture quite nicely the interaction between the local nature of events and the nonlocal nature of entanglement. But the earlier work ran into the problem that it could not handle all possible examples of evolution. Several specific examples were given. The problem was that over the course of a system evolving, two particles which had been unentangled can become entangled due to an event that is nonlocal to either. The simple linear logic calculus had no effective way to encode this situation. A solution was proposed, using something the authors called entanglement update, but it was felt at the time that more subtle encoding, using more connectives, should be possible.

Thus enters the new system of logics which go under the general name deep inference. Deep inference is a new methodology in proof theory, introduced in [START_REF] Guglielmi | A system of interaction and structure[END_REF] for expressing the logic BV, and subsequently developed to the point that all major logics can be expressed with deep-inference proof systems (see [START_REF] Guglielmi | Deep inference[END_REF] for a complete overview). Deep inference is more general than traditional Gentzen proof theory because proofs can be freely composed by the logical operators, instead of having a rigid formula-directed tree structure. This induces a new symmetry, which can be exploited for achieving locality of inference rules, and which is not generally achievable with Gentzen methods. Locality, in turn, makes it possible to use new methods, often with a geometric flavour, in the normalisation theory of proof systems.

Remarkably, the additional expressive power of deep inference turns out to be precisely what is needed to fully encode the sort of discrete quantum evolution that the first paper attempted to describe. The key is the noncommutativity of the added connective seq. This gives a method of encoding causal precedence directly into the syntax in a way that the original encoding of [START_REF] Blute | Discrete quantum causal dynamics[END_REF] using only linear logic lacked. This is the content of Theorem 4, which asserts that there is a precise correspondence between locative slices and derivable strings of formulas in the BV logic. This technical result is of independent interest beyond its use here.

Evolving quantum systems along directed acyclic graphs

In earlier work [START_REF] Blute | Discrete quantum causal dynamics[END_REF], the basis of the representation of quantum evolution was the graph of events and causal links between them. An event could be one of the following: a unitary evolution of some subsystem, an interaction of a subsystem with a classical device (a measurement) or perhaps just the coming together or splitting apart of several spatially separated subsystems. Events will be depicted as vertices of a directed graph. The edges of the graph will represent a physical flow between the different events. The vertices of the graph are then naturally labelled with operators representing the corresponding events. We assume that there are no causal cycles; the underlying graph has to be a directed acyclic graph (DAG). A typical dag is shown in Fig 1 . The square boxes, the vertices of the dag, are events where interaction occurs. The labelled edges represent fragments of the system under scrutiny moving through spacetime. At vertex 3, for example, the components c and d come together, interact and fly apart as g and h. Each labelled edge has associated with it a Hilbert space and the state of the subsystem is represented by some density matrix. Each edge thus corresponds to a density matrix and each vertex to a physical interaction.

These dags of events could be thought of as causal graphs as they are an evident generalization of the causal sets of Sorkin [START_REF] Sorkin | Spacetime and causal sets[END_REF]. A causal set is simply a poset, with the partial order representing causal precedence. A causal graph encodes much richer structure. So in a causal graph, we ask: What are the allowed physical effects? On physical grounds, the most general transformation of density matrices is a completely positive, trace non-increasing map or superoperator for short; see, for example, Chapter 8 of [START_REF] Nielsen | Quantum Computation and Quantum Information[END_REF].

Density matrices are not just associated with edges, they are associated with larger, more distributed, subsystems as well. We need some basic terminology associated with dags which brings out the causal structure more explicitly. We say that an edge e immediately precedes f if the target vertex of e is the source vertex of f . We say that e precedes f , written e f if there is a chain of immediate precedence relations linking e and f , in short, "precedes" is the transitive closure of "immediately precedes". This is not quite a partial order, because we have left out reflexivity, but concepts like chain (a totally ordered subset) and antichain (a completely unordered subset) work as in partial orders. We use the word "slice" for an antichain in the precedence order. The word is supposed to be evocative of "spacelike slice" as used in relativity, and has exactly the same significance.

A density matrix is a description of a part of a system. Thus it makes sense to ask about the density matrix associated with a part of a system that is not localized at a single event. In our dag of figure 1 we can, for example, ask about the density matrix of the portion of the system associated with the edges d, e and f . Thus density matrices can be associated with arbitrary slices. Note that it makes no sense to ask for the density matrix associated with a subset of edges that is not a slice.

The Hilbert space associated with a slice is the tensor product of the Hilbert spaces associated with the edges. Given a density matrix, say ρ, associated with, for example, the slice d, e, f , we get the density matrix for the subslice d, e by taking the partial trace over the dimensions associated with the Hilbert space f .

One can now consider a framework for evolution. One possibility, considered in [START_REF] Markopoulou | Quantum causal histories[END_REF], is to associate data with maximal slices and propagate from one slice to the next. Here, maximal means that to add any other vertex would destroy the antichain property. One then has to prove by examining the details of each dynamical law that the evolution is indeed causal. For example, one would like to show that the event at vertex 4 does not affect the density matrix at edge j. With data being propagated on maximal slices this does not follow automatically. One can instead work with local propagation; one keeps track of the density matrices on the individual edges only. This is indeed guaranteed to be causal, unfortunately it loses some essential nonlocal correlations. For example, the density matrices associated with the edges h and i will not reflect the fact that there might be nonlocal correlation or "entanglement" due to their common origin in the event at vertex 2. One needs to keep track of the density matrix on the slice i, h and earlier on d, e.

The main contribution of [START_REF] Blute | Discrete quantum causal dynamics[END_REF] was to identify a class of slices, called locative slices, that were large enough to keep track of all non-local correlations but "small enough" to guarantee causality. Definition 1. A locative slice is obtained as the result of taking any subset of the initial edges (all of which are assumed to be independent) and then propagating through edges without ever discarding an edge.

In our running example, the initial slices are {a}, {b} and {a, b},. Just choosing for example the initial edge a as initial slice, and propagating from there gives the locatives slices {a}, {c}, {g, h}, {j, h}, {g, k}, and {j, h}.

In fact, the following is a convenient way of presenting the locative slices and their evolution 6 .

{a} {c} {g, h} {j, h} {g, k} {j, k} {b} {f, d, e} {f, g, h, e} {f, d, i} {f, g, h, i} {j, h, i} {f, g, k} {j, k} {a, b} {c, f, d, e} {g, h, f, e} {c, f, d, i} {f, g, h, i} {f, g, h, i} {j, h, i} {f, g, k} {j, k}
Examples of non-locative slices are c, d, e and g, h, i and g, k. The intuition behind the concept of locativity is that one never discards information (by computing partial traces) when tracking the density matrices on locative slices. This is what allows them to capture all the non-local correlations.

The prescription for computing the density matrix on a given slice, say e, given the density matrices on the incoming slices and the superoperators at the vertices is to evolve from the minimal locative slice in the past of e to the minimal locative slice containing e. Any choice of locative slices in between may be used. The main results that we proved in [START_REF] Blute | Discrete quantum causal dynamics[END_REF] were that the density matrix so computed is (a) independent of the choice of the slicing (covariance) and (b) only events to the causal past can affect the density matrix at e (causality). Thus the dag and the slices form the geometrical structure and the density matrices and superoperators form the dynamics.

A First Logical View of Quantum Causal Evolution

The Logic of Directed Acyclic Graphs

One of the common interpretations of a dag is as generating a simple logic. (For readers not familiar with the approach to logic discussed here, we recommend [START_REF] Girard | Proofs and Types[END_REF].) The nodes of the dag are interpreted as logical sequents of the form:

A 1 , A 2 , . . . , A n B 1 , B 2 , . . . , B m

Here

is the logical entailment relation. Our system will have only one inference rule, called the Cut rule, which states:

Γ ∆, A A, Γ ∆ Γ, Γ ∆, ∆
Sequent rules should be interpreted as saying that if one has derived the two sequents above the line, then one can infer the sequent below the line. Proofs in the system always begin with axioms. Axioms are of the form A 1 , A 2 , . . . , A n B 1 , B 2 , . . . , B m , where A 1 , A 2 , . . . , A n are the incoming edges of some vertex in our dag, and B 1 , B 2 , . . . , B m will be the outgoing edges. There will be one such axiom for each vertex in our dag. For example, consider Figure 1. Then we will have the following axioms: Categorically, one can show that a dag canonically generates a free polycategory [START_REF] Szabo | Polycategories[END_REF], which can be used to present an alternative formulation of the structures considered here.

The Logic of Evolution

We need to make the link between derivability in our logic and locativity. This is not completely trivial. One could, naively, define a set ∆ of edges to be derivable if there is a deduction in the logic generated by G of Γ ∆ where Γ is a set of initial edges. But this fails to capture some crucial examples. For example, consider the dag underlying the system in Evidently, the set {f } is a locative slice, and yet the sequent a f is not derivable. The sequent a d, e is derivable, and one would like to cut it against d, e f , but one is only allowed to cut a single formula. Such "multicuts" are expressly forbidden, as they lead to undesirable logical properties [START_REF] Blute | Natural deduction and coherence for weakly distributive categories[END_REF].

Physically, the reason for this problem is that the sequent d, e f does not encode the information that the two states at d and e are correlated. It is precisely the fact that they are correlated that implies that one would need to use a multicut. To avoid this problem, one must introduce some notation, specifically a syntax for specifying such correlations. We will use the logical connectives of the multiplicative fragment of linear logic to this end [START_REF] Girard | Linear logic: Its syntax and semantics[END_REF]. The multiplicative disjunction of linear logic, denoted and called the par connective, will express such nonlocal correlations.

In our example, we will write the sequent corresponding to vertex 4 as d e f to express the fact that the subsystems associated with these two edges are possibly entangled through interactions in their common past.

Note that whenever two (or more) subsystems emerge from an interaction, they are correlated. In linear logic, this is reflected by the following rule called the (right) Par rule:

Γ ∆, A, B Γ ∆, A B
Thus we can always introduce the symbol for correlation in the right hand side of the sequent.

Notice that we can cut along a compound formula without violating any logical rules. So in the present setting, we would have the following deduction: All the cuts in this deduction are legitimate; instead of a multicut we are cutting along a compound formula in the last step. So the first step in modifying our general prescription is to extend our dag logic, which originally contained only the cut rule, to include the connective rules of linear logic.

The above logical rule determines how one introduces a par connective on the righthand side of a sequent. For the lefthand side, one introduces pars in the axioms by the following general prescription.

Given a vertex in a multigraph, we suppose that it has incoming edges a 1 , a 2 , . . . , a n and outgoing edges b 1 , b 2 , . . . , b m . In the previous formulation, this vertex would have been labelled with the axiom Γ = a 1 , a 2 , . . . , a n b 1 , b 2 , . . . , b m . We will now introduce several pars ( ) on the lefthand side to indicate entanglements of the sort described above. Begin by defining a relation ∼ by saying a i ∼ a j if there is an initial edge c and directed paths from c to a i and from c to a j . This is not an equivalence relation, but one takes the equivalence relation generated by the relation ∼. Call this new relation ∼ =. This relation partitions the set Γ into a set of equivalence classes. One then "pars" together the elements of each equivalence class, and this determines the structure of the lefthand side of our axiom. For example, consider vertices 5 and 6 in Figure 1. Vertex 5 would be labelled by f g j and vertex 6 would be labelled by h i k. On the other hand, vertex 3 would be labelled by c, d g, h.

Just as the par connective indicates the existence of past correlations, we use the more familiar tensor symbol ⊗, which is also a connective of linear logic, to indicate the lack of nonlocal correlation. This connective also has a logical rule:

Γ ∆, A Γ ∆ , B Γ, Γ ∆, ∆ , A ⊗ B
But we note that unlike in ordinary logic, this rule can only be applied in situations that are physically meaningful.

Definition 2. π : Γ ∆ and π : Γ ∆ are spacelike separated if the following two conditions are satisfied:

-Γ and Γ are disjoint subsets of the set of initial edges.

-The edges which make up ∆ and ∆ are pairwise spacelike separated.

In our extended dag logic, we will only allow the tensor rule to be applied when the two deductions are space like separated.

Summarizing, to every dag G we associate its "logic", namely the edges are considered as formulas and vertices are axioms. We have the usual linear logical connective rules, including the cut rule which in our setting is interpreted physically as propagation. The par connective denotes correlation, and the tensor lack of correlation. Note that every deduction in our system will conclude with a sequent of the form Γ ∆, where Γ is a set of initial edges. Now one would like to modify the definition of derivability to say that a set of edges ∆ is derivable if in our extended dag logic, one can derive a sequent Γ ∆ such that the list of edges appearing in ∆ was precisely ∆, and Γ is a set of initial edges. However this is still not sufficient as an axiomatic approach to capturing all locative slices. We note the example in Figure 3.

f3 f1 f4 f2 3 Q Q Q Q Q Q Q Q Q Q k d h
Evidently the slice {f, g} is locative, but we claim that it cannot be derived even in our extended logic. To this directed graph, we would associate the following axioms: a c, h b d, e c, d f h, e g

Note that there are no correlations between c and d or between h and e. Thus no -combinations can be introduced. Now if one attempts to derive a, b f, g, we proceed as follows:

a c, h b d, e a, b c ⊗ d, h, e c, d f c ⊗ d f a, b h, e, f
At this point, we are unable to proceed. Had we attempted the symmetric approach tensoring h and e together, we would have encountered the same problem.

The problem is that our logical system is still missing one crucial aspect, and that is that correlations develop dynamically as the system evolves, or equivalently as the deduction proceeds. We note that this logical phenomenon is reflected in physically occurring situations. But a consequence is that our axioms must change dynamically as well. This seems to be a genuinely new logical principle.

We give the following definition. Definition 3. Suppose we have a deduction π of the sequent Γ ∆ in the logic associated to the dag G, and that T is a vertex in G to the future or acausal to the edges of the set ∆ with a and b among the incoming edges of T . Then a and b are correlated with respect to π if there exist outgoing edges c and d of the proof π and directed paths from c to a and from d to b.

So the point here is that when performing a deduction, one does not assign an axiom to a given vertex until it is necessary to use that axiom in the proof. Then one assigns that axiom using this new notion of correlation and the equivalence relation defined above. This prescription reflects the physical reality that entanglement of local quantum subsystems could develop as a result of a distant interaction between some other subsystems of the same quantum system. We are finally able to give the following crucial definition: Definition 4. A set ∆ of edges in a dag G is said to be derivable if there is a deduction in the logic associated to G of Γ ∆ where ∆ is a sequence of formulas whose underlying set of edges is precisely ∆ and where Γ is a set of initial edges, in fact the set of initial edges to the past of ∆. Theorem 1. A set of edges is derivable if and only if it is locative. More specifically, if there is a deduction of Γ ∆ as described above, then ∆ is necessarily locative. Conversely, given any locative slice, one can find such a deduction.

Proof. Recall that a locative slice L is obtained from the set of initial edges in its past by an inductive procedure. At each step, we choose arbitrarily a minimal vertex u in the past of L, remove the incoming edges of u and add the outgoing edges. This step corresponds to the application of a cut rule, and the method we have used of assigning the par connective to the lefthand side of an axiom ensures that it is always a legal cut. The tensor rule is necessary in order to combine spacelike separated subsystems in order to prepare for the application of the cut rule.

Thus we have successfully given an axiomatic logic-based approach to describing evolution. In summary, to find the density matrix associated to a locative slice ∆, one finds a set of linear logic formulas whose underlying set of atoms is ∆ and a deduction of Γ ∆ where Γ is as above.

Using Deep Inference to Capture Locativity

In the previous sections we explained the approach of [START_REF] Blute | Discrete quantum causal dynamics[END_REF], using as key unit of deduction a sequent a 1 , . . . , a k b 1 , . . . , b l meaning that the slice {b 1 , . . . , b l } is reachable from {a 1 , . . . , a k } by firing a number of events (vertices). However, this approach is not able to entirely capture the notion of locative slices, because correlations develop dynamically as the system evolves, or equivalently, as the deduction proceeds. Thus, we had to let axioms evolve dynamically.

The deep reason behind this problem is that the underlying logic is multiplicative linear logic (MLL): The sequent above represents the formula a

1 • • • a k b 1 • • • b l or equivalently a ⊥ 1 • • • a ⊥ k b 1 • • • b l , i.e
., the logic is not able see the aspect of time in the causality. For this reason we propose to use the logic BV, which is essentially MLL (with mix) enhanced by a third binary connective (called seq or before) which is associative and non-commutative and self-dual, i.e., the negation of A B is A ⊥ B ⊥ . It is this non-commutative connective, which allows us to properly capture quantum causality.

Of course, we are interested in expressing our logic in a deductive system that admits a complete cut-free presentation. In this case, as we briefly argue in the following, the adoption of deep inference is necessary to deal with a self-dual non-commutative logical operator.

Review of BV and Deep Inference

The significance of deep inference systems was discussed in the introduction. We note now that within the range of the deep-inference methodology, we can define several formalisms, i.e. general prescriptions (like the sequent calculus or natural deduction) on how to design proof systems. The first, and conceptually simplest, formalism that has been defined in deep inference is called the calculus of structures, or CoS, and this is what we adopt in this paper and call "deep inference". In fact, the fine proof-theoretic points about the various deep inference formalisms are not relevant to this paper.

The proof theory of deep inference is now well developed for classical [START_REF] Brünnler | Locality for classical logic[END_REF], intuitionistic [START_REF] Tiu | A local system for intuitionistic logic[END_REF][START_REF] Guenot | Nested Deduction in Logical Foundations for Computation[END_REF], linear [START_REF] Straßburger | A local system for linear logic[END_REF][START_REF] Straßburger | MELL in the calculus of structures[END_REF] and modal [START_REF] Brünnler | Deep sequent systems for modal logic[END_REF][START_REF] Straßburger | Cut elimination in nested sequents for intuitionistic modal logics[END_REF] logics. More relevant to us, there is an extensive literature on BV and commutative/non-commutative linear logics containing BV. We cannot here provide a tutorial on BV, so we refer to its literature. In particular, [START_REF] Guglielmi | A system of interaction and structure[END_REF] provides the semantic motivation and intuition behind BV, together with examples of its use. In [START_REF] Tiu | A system of interaction and structure II: The need for deep inference[END_REF], Tiu shows that deep inference is necessary for giving a cut-free deductive system for the logic BV. Kahramanogulları proves that System BV is NP-complete [START_REF] Kahramanogulları | System BV is NP-complete[END_REF].

We now proceed to define system BV, quickly and informally. The inference rules are:

F {•} ai↓ F {a a ⊥ } F {A [B C]} s F {(A B) C} F {a a ⊥ } ai↑ F {•} F {[A C] [B D]} q↓ F { A B C D } F { A B C D } q↑ F {(A C) (B D)}
They have to be read as ordinary rewrite rules acting on the formulas inside arbitrary contexts F { }. Note that we push negation via DeMorgan equalities to the atoms, and thus, all contexts are positive. The letters A, B, C, D stand for arbitrary formulas and a is an arbitrary atom. Formulas are considered equal modulo the associativity of all three connectives , , and , the commutativity of the two connectives and , and the unit laws for •, which is unit to all three connectives, i.e.,

A = A • = A • = A • = • A.
Since, in our experience, working modulo equality is a sticky point of deep inference, we invite the reader to meditate on the following examples which are some of the possible instances of the q↓ rule: The best way to understand the rules of BV is to learn their intuitive meaning, which is explained by an intuitive "space-temporal" metaphor in [START_REF] Guglielmi | A system of interaction and structure[END_REF].

The set of rules {ai↓, ai↑, s, q↓, q↑} is called SBV, and the set {ai↓, s, q↓} is called BV. We write

A ∆ SBV B
to denote a derivation ∆ from premise A to conclusion B using SBV, and we do analogously for BV.

Much like in the sequent calculus, we can consider BV a cut-free system, while SBV is essentially BV plus a cut rule. The two are related by the following theorem.

Theorem 2. For all formulas A and B, we have

A SBV B if and only if • BV A ⊥ B .
Again, all the details are explained in [START_REF] Guglielmi | A system of interaction and structure[END_REF]. Let us here only mention that the usual cut elimination is a special case of Theorem 2, for A = •. Then it says that a formula B is provable in BV iff it is provable in SBV.

Observation 3 If a formula A is provable in BV, then every atom a occurs as often in A as a ⊥ . This is easy to see: the only possibility for an atom a to disappear is in an instance of ai↓; but then at the same time an atom a ⊥ disappears. Definition 5. A BV formula Q is called a negation cycle if there is a nonempty set of atoms P = {a 0 , a 2 , . . . , a n-1 }, such that no two atoms in P are dual, i = j implies a i = a j , and such that

Q = Z 0 • • • Z n-1
, where, for every j = 0, . . . , n -1, we have Z j = a j a ⊥ j+1 (mod n) or Z j = a j a ⊥ j+1 (mod n) . We say that a formula P contains a negation cycle if there is a negation cycle Q such that -Q can be obtained from P by replacing some atoms in P by •, and all the atoms that occur in Q occur only once in P .

Example 1. The formula (a c [d ⊥ b]) c ⊥ b ⊥ [a ⊥ d] contains a nega- tion cycle (a b) b ⊥ a ⊥ = (a • [• b]) • b ⊥ [a ⊥ •] .
Proposition 1. Let A be a BV formula. If P contains a negation cycle, then P is not provable in BV.

A proof of this propostion can be found in [START_REF] Straßburger | Linear Logic and Noncommutativity in the Calculus of Structures[END_REF]Proposition 7.4.30]. A symmetric version of this proposition has been shown for SBV in [START_REF] Straßburger | A system of interaction and structure IV: The exponentials and decomposition[END_REF]Lemma 5.20].

Locativity Via BV

Let us now come back to dags. A vertex v ∈ V in such a graph G = (V , E ) is now encoded by the formula

V = (a ⊥ 1 • • • a ⊥ k ) [b 1 • • • b l ]
where {a 1 , . . . , a k } = target -1 (v) is the set of edges having their target in v, and {b 1 , . . . , b l } = source -1 (v) is the set of edges having their source in v. For a slice S = {e 1 , . . . , e n } ⊆ E we define its encoding to be the formula S = e 1 • • • e n .

Lemma 1. Let (V , E ) be a dag, let S ⊆ E be a slice, let v ∈ V be such that target -1 (v) ⊆ S , and let S be the propagation of S through v. Then there is a derivation

S V SBV S (1)
where V , S, and S are the encodings of v, S , and S , respectively.

[e1 • • • em a1 • • • a k ] (a ⊥ 1 • • • a ⊥ k ) [b1 • • • b l ] s e1 • • • em ([a1 • • • a k ] (a ⊥ 1 • • • a ⊥ k ) [b1 • • • b l ] ) q↑ e1 • • • em ([a1 • • • a k ] a ⊥ 1 • • • a ⊥ k ) [b1 • • • b l ] s e1 • • • em ([(a1 a ⊥ 1 ) a2 • • • a k ] • • • a ⊥ k ) [b1 • • • b l ] ai↑ e1 • • • em ([a2 • • • a k ] a ⊥ 2 • • • a ⊥ k ) [b1 • • • b l ] s . . . ai↑ e1 • • • em ([a k-1 a k ] a ⊥ k-1 a ⊥ k ) [b1 • • • b l ] s e1 • • • em ([(a k-1 a ⊥ k-1 ) a k ] a ⊥ k ) [b1 • • • b l ] ai↑ e1 • • • em (a k a ⊥ k ) [b1 • • • b l ] ai↑ e1 • • • em • [b1 • • • b l ] = , e1 • • • em b1 • • • b l as desired.
Lemma 2. Let (V , E ) be a dag, let S , S ⊆ E be slices, such that S is reachable from S by firing a number of events (vertices). Then there is a derivation

S V 1 • • • V n SBV S (2)
where V 1 , . . . , V n encode v 1 , . . . , v n ∈ V (namely, the vertices through which the slices are propagated), and S, S encode S , S .

Proof. If S is reachable from S then there is an n ≥ 0 and slices S 0 , . . . , S n ⊆ E and vertices v 1 , . . . , v n ∈ V such that for all i ∈ {1, . . . , n} we have that S i is the propagation of S i-1 through v i , and S = S 0 and S = S n . Now we can apply Lemma 1 n times to get the derivation (2). Lemma 3. Let (V , E ) be a dag, let S and S be the encodings of S , S ⊆ E , where S is a slice. Further, let V 1 , . . . , V n be the encodings of v 1 , . . . , v n ∈ V . If there is a proof

- Π BV V ⊥ 1 • • • V ⊥ n S ⊥ S
then S is a slice reachable from S and v 1 , . . . , v n are the vertices through which it is propagated.

Proof. By induction on n. If n = 0, we have a proof of S ⊥ S . Since S ⊥ contains only negated propositional variables, and S only non-negated ones, we have that every atom in S has its killer in S ⊥ . Therefore S = S . Let now n ≥ 1. We can assume that S = e 1 • • • e m , and that for every i ∈ {1, . . . , n} we have

V ⊥ i = [a i1 • • • a iki ] (b ⊥ i1 • • • b ⊥ ili ).
i.e., target -1 (v i ) = {a i1 , . . . , a iki } and source -1 (v i ) = b i1 , . . . , b ili . Now we claim that there is an i ∈ {1, . . . , n} such that {b i1 , . . . , b ili } ⊆ {e 1 , . . . , e m }. In other words, there is a vertex among the v 1 , . . . , v n , such that all its outgoing edges are in S . For showing this claim assume by way of contradiction that every vertex among v 1 , . . . , v n has an outgoing edge that does not appear in S , i.e., for all i ∈ {1, . . . , n}, there is an s i ∈ 1, . . . , l i with b isi / ∈ {e 1 , . . . , e m }. By Observation 3, we must have that for every i ∈ {1, . . . , n} there is a j ∈ {1, . . . , n} with b isi ∈ {a j1 , . . . , a jkj }, i.e., the killer of b ⊥ isi occurs as incoming edge of some vertex v j . Let jump : {1, . . . , n} → {1, . . . , n} be a function that assigns to every i such a j (there might be many of them, but we pick just one). Now let i 1 = 1, i 2 = jump(i 1 ), i 3 = jump(i 2 ), and so on. Since there are only finitely many V i , we have an p and q with p ≤ q and i q+1 = i p . Let us take the minimal such q, i.e., i p , . . . , i q are all different. Inside the proof Π above, we now replace everywhere all atoms by •, except for b ip , b ⊥ ip , . . . , b iq , b ⊥ iq . By this, the proof remains valid and has conclusion

b iq b ⊥ ip b ip b ⊥ ip+1 • • • b iq-1 b ⊥ iq ,
which is a contradiction to Proposition 1. This finishes the proof of the claim. Now we can, without loss of generality, assume that v n is the vertex with all its outgoing edges in S , i.e., {b n1 , . . . , b nln } ⊆ {e 1 , . . . , e m }, and (again without loss of generality) e 1 = b n1 , . . . , e ln = b nln . Our proof Π looks therefore as follows:

- Π BV V ⊥ 1 • • • V ⊥ n-1 S ⊥ [a n1 • • • a nkn ] (b ⊥ n1 • • • b ⊥ nln ) V ⊥ n S where S = b n1 • • • b nln e ln+1
- Π BV V ⊥ 1 • • • V ⊥ n-1 S ⊥ a n1 • • • a nkn e ln+1 • • • e m
to which we can apply the induction hypothesis, from which we can conclude that S = {a n1 , . . . , a nkn , e ln+1 , . . . , e m } is a slice that is reachable from S. Clearly S is the propagation of S through v n , and therefore it is a slice and reachable from S .

Theorem 4. Let G = (V , E ) be a dag. A subset S ⊆ E is a locative slice if and only if there is a derivation

I V 1 . . . V n SBV S ,
where S is the encoding of S , and I is the encoding of a subset of the initial edges, and V 1 , . . . , V n encode v 1 , . . . , v n ∈ V .

Proof. The "only if" direction follows immediately from Lemma 2. For the "if" direction, we first apply Theorem 2, and then Lemma 3.

Conclusion

Having a logical syntax also leads to the possibility of discussing semantics; this would be a mathematical universe in which the logical structure can be interpreted. This has the potential to be of great interest in the physical systems we are considering here, where one would want to calculate such things as expectation values. As in any categorical interpretation of a logic, one needs a category with appropriate structure to support the logical connectives and model the inference rules. The additional logical connectives of BV allows for more subtle encodings than can be expressed in a compact closed category. The structure of BV leads to interesting category-theoretic considerations [START_REF] Blute | Deep inference and probabilistic coherence spaces[END_REF]. One must find a category with the following structure:

- * -autonomous structure, i.e. the category must be symmetric, monoidal closed and self-dual. an additional (noncommutative) monoidal structure commuting with the above duality. coherence isomorphisms necessary to interpret the logic, describing the interaction of the various tensors.

Such categories are called BV-categories in [START_REF] Blute | Deep inference and probabilistic coherence spaces[END_REF]. Of course, trivial examples abound. One can take the category Rel of sets and relations, modelling all three monoidal structures as one. Similarly the category of (finite-dimensional) Hilbert spaces, or any symmetric compact closed category would suffice. But what is wanted is a category in which the third monoidal structure is genuinely noncommutative.

While this already poses a significant challenge, we are here faced with the added difficulty that we would like the category to have some physical significance, to be able to interpret the quantum events described in this paper. Fortunately, work along these lines has already been done. See [START_REF] Blute | Deep inference and probabilistic coherence spaces[END_REF].

That paper considers the category of Girard's probabilistic coherence spaces PCS, introduced in [START_REF] Girard | Number 316 in LMS Lecture Note Series[END_REF]. While Girard demonstrates the * -autonomous structure, the paper [START_REF] Blute | Deep inference and probabilistic coherence spaces[END_REF] shows that the category properly models the additional noncommutative tensor of BV. We note that the paper [START_REF] Girard | Number 316 in LMS Lecture Note Series[END_REF] also has a notion of quantum coherence space, where analogous structure can be found.

Roughly, a probabilistic coherence space is a set X equipped with a set of generalized measures, i.e. functions to the set of nonnegative reals. These are called the allowable generalized measures. The set must be closed with respect to the double dual operation, where duality is determined by polarity, where we say that two generalized measures on X are polar, written f ⊥ g, if x∈X f (x)g(x) ≤ 1

The noncommutative connective is then modelled by the formula:

A B = { n i=1 f i ⊗ g i | f
i is an allowable measure on A and n i=1 g i is an allowable measure on B } Note the lack of symmetry in the definition. Both the categories of probabilistic and quantum coherence spaces will likely provide physically interesting semantics of the discrete quantum dynamics presented here. We hope to explore this in future work.

Fig. 1 .

 1 Fig. 1. A dag of events

6 k

 6 where we have labelled each entailment symbol with the name of the corresponding vertex. The following is an example of a deduction in this system of the sequent a, b f, g, h, i. b d, e, f a c c, d g, h a, d g, h a, b e, f, g, h e i a, b f, g, h, i

Figure 2 .

 2 Corresponding to this dag, we get the following basic morphisms (axioms): a b, c b d c e d, e f.

  Fig. 2.

  Fig. 3.

  By referring to the previously defined q↓ rule scheme, we can see that the second instance above is produced by takingF { } = { }, A =a b e, B = •, C = c and D = d, and the third instance is produced by taking F { } = { } e, A = c d, B = •, C = • and D = a b.

Proof.

  Assume source -1 (v) = {b 1 , . . . , b l } and target -1 (v) = {a 1 , . . . , a k } and S = {e 1 , . . . , e m , a 1 , . . . , a k }. Then S = {e 1 , . . . , e m , b 1 , . . . , b l }. Now we can construct

  • • • e m . In Π we can now replace the atoms b n1 , b ⊥ n1 , . . . , b nln , b ⊥ nln everywhere by •. This yields a valid proof

We thank an anonymous referee for this presentation.

Acknowledgements

Research supported in part by NSERC, by the ANR project "INFER" and the INRIA ARC "Redo".