{'fraction_non_alphanumeric': 0.04963898916967509, 'fraction_numerical': 0.008400444321021938, 'mean_word_length': 4.079771476936098, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 2, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
The Geometry of Parallelism. Classical, Probabilistic, and Quantum Effects

We introduce a Geometry of Interaction model for higher-order quantum computation, and prove its adequacy for a full quantum programming language in which entanglement, duplication, and recursion are all available. Our model comes with a multi-token machine, a proof net system, and a PCF-style language. The approach we develop is not specific to quantum computation, and our model is an instance of a new framework whose main feature is the ability to model commutative effects in a parallel setting. Being based on a multi-token machine equipped with a memory, it has a concrete nature which makes it well suited for building low-level operational descriptions of higher-order languages.


Introduction
In classical computation, information is deterministic, discrete and freely duplicable. Already from the early days [1], however, determinism has been relaxed by allowing state evolution to be probabilistic. The classical model has then been further challenged by quantum computation [2], a computation paradigm which is based on the laws of quantum mechanics.
Probabilistic and quantum computation are both justified by the very efficient algorithms they give rise to: think about Miller-Rabin primality test [3,4], Shor's factorization [5] but also the more recent algorithms for quantum chemistry [6] or for solving linear systems of equations [7]. Finding out a way to conveniently express those algorithms without any reference to the underlying hardware, is then of paramount importance.
This has stimulated research on programming languages for probabilistic [8,9] and quantum computation (see [10] for a survey), and recently on higher-order functional languages [11][12][13]. The latter has been epitomized by variations and extensions of the λ-calculus. In order to allow compositional reasoning, it is important to give a denotational semantics to those languages; maybe surprisingly, a large body of works in this direction is closely connected to denotational and interactive models of Linear Logic [14], in the style of Game Semantics [15,16] and the Geometry of Interaction [17].
The case of quantum computation is emblematic. The first adequate denotational model for a quantum programming languageà la PCF, only two years old [13], marries a categorical construction for the exponentials of linear logic [18,19] to a suitable extension of the standard model of quantum computation: the category of completely positive maps [20]. The development of an interactive semantics has proved to be highly nontrivial, with results which are impressive but not yet completely satisfactory. In particular, the underlying language either does not properly reflect entanglement [21][22][23], a key feature of quantum computation, or its expressive power is too weak, lacking recursion and duplication [24,25]. The main reason for this difficulty lies in the inherent non-locality of entanglement [2].
In this paper we show that Girard's Geometry of Interaction (GoI) indeed offers the right tools to deal with a fully fledged quantum programming language in which duplication and full recursion are available, when we equip GoI with an external quantum memory, a standard technique for operational models of quantum λ-calculi [11].
We go further: the approach we develop is not specific to quantum computation, and our quantum model is introduced as an instance of a new framework which models choice effects in a parametric way, via a memory structure. The memory structure comes with three operations: (1) allocation of fresh addresses in the memory, (2) low-level actions on the memory, and (3) choice based on the value of the memory at a given address. The notion of memory structure is flexible, the only requirement being commutativity of the operations. In Sec. 3.3 we show that different kinds of choice effects can be systematically treated: classical, probabilistic and quantum memory are all instances of this general notion. Therefore, the memory makes the model suitable to interpret classical, probabilistic and quantum functional programs. In particular, in the case of quantum memory, a low-level action is an application of unitary gate to the memory, while the choice performs a quantum measure.
The GoI model we give has a very concrete nature, as it consists of a class of token machines [26,27]. Their distinctive feature is to be parallel and multi-token [25,28] rather than single-token as in classic token machines [26]. Being multi-token means that different computational threads can interact with each other and synchronize (think of this as a multi-player game, where players are able to collaborate and exchange information). The presence of multiple tokens allows to appropriately reflect non-locality in a quantum setting, but also to generally deal with parallelism and choice effects in a satisfactory way. We discuss why this is the case when we concretely present the machine (Sec. 5).
Finally, to deal with the combination of parallelism, probabilistic side-effects and non-termination, we develop a general notion of PARS, probabilistic abstract rewrite system. The results we establish on PARS are the key ingredient in the Adequacy proofs, but are also of independent interest. The issues at sake are non-trivial and we discuss them in the dedicated Sec. 1.2.
Contributions. We present a Geometry of Interaction (GoI) model for higher-order quantum computation, which is adequate for a quantum programming language in which entanglement, duplication, and recursion are all available. Our model comes with a multitoken machine, a proof net system, and a PCF-style language. More specifically, this paper's contributions can be summarized as follows: • we equip GoI with the ability to capture choice effects using a parametric notion of memory structure (Sec. 3); • we show that the notion of memory structure is able to capture classical, probabilistic and quantum effects (Sec. 3.3); • we introduce a construction which is parametric on the memory, and produces a class of multi-token machines (Sec. 5), proof net systems (Sec. 4) and PCF-style languages (Sec. 6). We prove that (regardless of the specific memory) the multi-token machine is an adequate model of nets reduction (Th. 28), and the nets an adequate model of PCF term rewriting (Th. 29); • we develop a general notion of parallel abstract rewrite system, which allows us to deal with the combination of parallelism and probabilistic choice in an infinitary setting (Sec. 2). Being based on a multi-token machine associated to a memory, our model has a concrete nature which makes it well suited to build low-level operational descriptions of higher-order programming languages. In the remainder of this section, we give an informal overview of various aspects of our framework, and motivate with some examples the significance of our contribution.
This report is an extended version of [29].

Geometry of Interaction and Quantum Computation
Geometry of Interaction is interesting as semantics for programming languages [27,30,31] because it is a high-level semantics which at the same time is close to low-level implementation and has a clear operational flavor. Computation is interpreted as a flow of information circulating around a network, which essentially is a representation of the underlying program. Computational steps are broken into low-level actions of one or more tokens which are the agents carrying the information around.
A long standing open question is whether fully fledged higher-order quantum computation can be modeled operationally via the Geometry of Interaction.

Quantum Computation
As comprehensive references can be found in the literature [2], we only cover the very few concepts that will be needed in this paper. Quantum computation deals with quantum bits rather than bits. The state of a quantum system can be represented with a density matrix to account for its probabilistic nature. However for our purpose we shall use in this paper the usual, more operational, non-probabilistic representation. Single quantum bits (or qubits) will thus be represented by a ray in a two-dimensional complex Hilbert space, that is, an equivalence class of non-zero vectors up to (complex) scalar multiplication. Information is attached to a qubit by choosing an orthonormal basis (|0 , |1 ): a qubit is a superposition of two classical bits (modulo scalar multiplication). If the state of several bits is represented with the product of the states of single bits, the state of a multi-qubit system is represented with the tensor product of single-qubit states. In particular, the state of an n-qubit system is a superposition of the state of an n-bit system. We consider superpositions to be normalized. Two kinds of operations can be performed on qubits. First, one can perform reversible, unitary gates: they are unitary maps in the corresponding Hilbert space. A more exotic operation is the measurement, which is the only way to retrieve a classical bit out of a quantum bit. This operation is probabilistic: the probabilities depend on the state of the system. Moreover, it modifies the state of the memory. Concretely, if the original memory state is α0|0 ⊗φ0+α1|1 ⊗φ1 (with φ0 and φ1 normalized), measuring the first qubit would answer x with probability |αx| 2 , and the memory is turned into |x ⊗ φx. Note how the measurement not only modifies the measured qubit, but also collapses the global state of the memory.
The effects of measurements are counterintuitive especially in entangled system: consider the 2-qubit system √ 2 2 (|00 + |11 ). This system is entangled, meaning that it cannot be written as φ ⊗ ψ with 1-qubit states φ and ψ. One can get such a system from the state |00 by applying first an Hadamard gate H on the second qubit, sending |0 to , therefore getting the state √ 2 2 (|00 +|01 ), and then a CNOT (controlled-not) gate, sending |xy to |x ⊕ y ⊗ |y . Measuring the first qubit will collapse the entire system to |00 or |11 , with equal probability 1 2 . Remark 1. Notwithstanding the global collapse induced by the measurement, the operations on physically disjoint quantum states are commutative. Let A and B be two quantum states. Let U act on A and V act on B (whether they are unitaries, measurements, or combinations thereof). Consider now A ⊗ B: applying U on A then V on B is equivalent to first applying V on B and then A on U . In other words, the order of actions on physically separated quantum systems is irrelevant. We use this property in Sec. 3.3.3.

Previous Attempts and Missing Features
A first proposal of Geometry of Interaction for quantum computation is [21]. Based on a purely categorical construction [32], it features duplication but not general entanglement: entangled qubits cannot be separately acted upon. As the authors recognize, a limit of their approach is that their GoI is single-token, and they already suggest that using several tokens could be the solution.
cannot be represented in [21], because it is not possible to send entangled qubits to separate parts of the program.
A more recent proposal [25], which introduces an operational semantics based on multi-tokens, can handle general entanglement. However, it does neither handle duplication nor recursion. More than that, the approach relies on termination to establish its results, which therefore do not extend to an infinitary setting: it is not enough to "simply add" duplication and fix points.
Example 3. In [25] it is not possible to simulate the program that tosses a coin (by performing a measurement), returns a fresh qubit on head and repeats on tail. In mock-up ML, this program becomes where new creates a fresh qubit in state |0 and where the if test performs a measurement on the qubit x. Note how the measure of H new amounts to tossing a fair coin: H new produces √ 2 2 (|0 +|1 ). Measuring gives |0 and |1 with probability 1 2 . Example 3 will be our leading example all along the paper. Furthermore, we shall come back to both examples in Sec. 7.1.1.

Parallel Choices: Confluence and Termination
When dealing with both probabilistic choice and infinitary reduction, parallelism makes the study of confluence and convergence highly non-trivial. The issue of confluence arises as soon as choices and duplication are both available, and non-termination adds to the challenges. Indeed, it is easy to see how tossing a coin and duplicating the result does not yield the same probabilistic result as tossing twice the coin. To play with this, let us take for example the following term of the probabilistic λ-calculus [33]: M = (λx.x xor x)((tt ⊕ ff) ⊕ Ω) where tt and ff are boolean constants, Ω is a divergent term, ⊕ is the choice operator (here, tossing a fair coin), and xor is the boolean operator computing the exclusive or. Depending on which of the two redexes we fire first, M will evaluate to either the distribution {ff  In ordinary, deterministic PCF, any program of boolean type may or may not terminate, depending on the reduction strategy, but its normal form, if it exists, is unique. This is not the case for our probabilistic term M : depending on the choice of the redex, it evaluates to two distributions which are simply not comparable.
In the case of probabilistic λ-calculi, the way-out to this is to fix a reduction strategy; the issue however is not only in the syntax, it appears-at a more fundamental level-also in the model. This is the case for [33], where the model itself does not support parallel probabilistic choice. Similarly, in the development of a Game Semantics or Geometry of Interaction model for probabilistic λ-calculi, the standard approach has been to use a polarized setting, so to impose a strict form of sequentiality [34,35]. If instead we choose to have parallelism in the model, confluence is not granted and even the definition of convergence is non-trivial.
In this paper we propose a probabilistic model that is infinitary and parallel but confluent; to achieve this, in Sec. 2 we develop some results which are general to any probabilistic abstract rewrite system, and which to our knowledge are novel. More specifically, we provide sufficient conditions for an infinitary probabilistic system to be confluent and to satisfy a property which is a probabilistic analogous of the familiar "weak normalization implies strong normalization". We then show that the parametric models which we introduce (both the proof nets and the multi-token machine) satisfy this property; this is indeed what ultimately grants the adequacy results.

Overview of the Framework, and Its Advantages
A quantum program has on one hand features which are specific to quantum computing, and on the other hand standard constructs. This is indeed the case for many paradigmatic languages; analyzing the features separately is often very useful. Our framework clearly separates (both in the language and in its operational model) the constructs which are common to all programming languages (e.g. recursion) and the features which are specific to some of them (e.g. measurement or probabilistic choice). The former is captured by a fixed operational core, the latter is encapsulated within a memory structure. This approach has two distinctive advantages: • Facilitate Comparison between Different Languages: clearly separating in the semantics the standard features from the "notions of computation" which is the specificity of the language, allows for an easier comparison between different languages.
• Simplify the Design of a Language with Its Operational Model: it is enough to focus on the memory structure which encapsulates the desired effects. Once such a memory structure is given, the construction provides an adequate Geometry of Interaction model for a PCF-like language equipped with that memory. Memory structures are defined in Sec. 3, while the operational core is based on Linear Logic: a linearly-typed PCF-like language, Geometry of Interaction, and its syntactical counterpart, proof nets. Proof nets are a graph-based formal system that provides a powerful tool to analyze the execution of terms as a rewriting process which is mostly parallel, local, and asynchronous.
More in detail, our framework consists of: 1. a notion of memory structure, whose operations are suitable to capture a range of choice effects; 2. an operational core, which is articulated in the three base rewrite systems (a proof net system, a GoI multi-token machine, and a PCF-style language); 3. a construction which is parametric on the memory, and lifts each base rewrite system into a more expressive operational system. We respectively call these systems: program nets, MSIAM machines and PCF AM abstract machines. Finally, the three forms of systems are all related by adequacy results. As long as the memory operations satisfy commutativity, the construction produces an adequate GoI model for the corresponding PCF language. More precisely, we prove-again parametrically on the memory-that the MSIAM is an adequate model of program net reduction (Th. 28), and program nets are expressive enough to adequately represent the behavior of the PCF language (Th. 29).

Related Work
The low-level layer of our framework can be seen as a generalization and a variation of systems which are in the literature. The nets and multi-token machine we use are a variation of [28], the linearly typed PCF language is the one in [13] (minus lists and coproducts). What we add in this paper are the right tools to deal with challenges like probabilistic parallel reduction and entanglement. Neither quantum nor probabilistic choice can be treated in [28], because of the issues we clarified in Sec. 1.2. The specificity of our proposal is really its ability to deal with choice together with parallelism.
We already discussed previous attempts to give a GoI model of quantum computation, and their limits, in Sec. 1.1.2 above. Let us quickly go through other models of quantum computation. Our parametric memory is presented equationally: equational presentations of quantum memory are common in the literature [36,37]. Other models of quantum memories are instead based on Hilbert spaces and completely positive maps, as in [13,20]. In both of these approaches, the model captures with precision the structure and behavior of the memory. Instead, in our setting, we only consider the interaction between the memory and the underlying computation by a set of equations on the state of the memory at a given address, the allocation of fresh addresses, and the low-level actions.
Finally, taking a more general perspective, our proposal is by no means the first one to study effects in an interactive setting. Dynamic semantics such as GoI and Game Semantics are gaining interest and attention as semantics for programming languages because of their operational flavor. [35,38,39] all deal with effects in GoI. A common point to all these works is to be single-token. While our approach at the moment only deals with choice effects, we indeed deal with parallelism, a challenging feature which was still missing.

PARS: Probabilistic Abstract Reduction Systems
Parallelism allows critical pairs; as we observed in Sec. 1.2, firing different redexes will produce different distributions and can lead to possibly very different results. Our parallel model however enjoys a property similar to the diamond property of abstract rewrite systems. Such a property entails a number of important consequences for confluence and normalization, and these results in fact are general to any probabilistic abstract reduction system. In particular, we define what we mean by strong and weak normalization in a probabilistic setting, and we prove that a suitable adaptation of the diamond property guarantees confluence and a form of uniqueness of normal forms, not unlike what happens in the deterministic case. Th. 11 is the main result of the section. In a probabilistic context, spelling out the diamond property requires some care. We will introduce a strongly controlled notion of reduction on distributions (⇒). The need for this control has the same roots as in the deterministic case: please recall that strong normalization follows from weak normalization by the diamond ) which appears very similar, but "leaves space" for an infinite branch.

Distributions and PARS
We start by setting the basic definitions. Given a set A, we note DST (A) for the set of probability distributions on A: any µ ∈ DST (A) is a function from A to [0, 1] such that a∈A µ(a) ≤ 1.
A distribution µ is proper if a∈A µ(a) = 1. The distribution assigning 0 to each element of a set A is indicated with 0. We indicate with SUPP (µ) the support of a distribution µ, i.e. the subset of A whose image under µ is not 0. On DST (A), we define the relation ⊆ point-wise: µ ⊆ ρ if µ(a) ≤ ρ(a) for each a ∈ A.
A probabilistic abstract reduction system (PARS) is a pair A = (A, →) consisting of a set A and a relation → ⊆ A × DST (A) (rewrite relation, or reduction relation) such that for each (a, µ) ∈ →, SUPP (µ) is finite. We write a → µ for (a, µ) ∈ →. An element a ∈ A is terminal or in normal form (w.r.t. →) if there is no µ with a → µ, which we write a →.
We can partition any distribution µ into a distribution µ • on terminal elements, and a distributionμ on elements for which there exists a reduction, as follows: The degree of termination of µ, written T (µ), is a∈A µ • (a). We write for the reflexive and transitive closure of →, namely the smallest subset of A × DST (A) closed under the following rules: µ + p · ρ We read a µ as "a reaches µ". The Relation ⇒ ⇒ ⇒. In order to extend to PARS classical results on termination for rewriting systems, we define the binary relation ⇒, which lifts the notion of one step reduction to distributions: we require that all non-terminal elements are indeed reduced. The Please note that in the derivation above, we require a → ρa for each a ∈ SUPP (μ). Observe also that µ • ⇒ µ • since SUPP (μ • ) = ∅.
We write µ ⇒ n ρ if µ reduces to ρ in n ≥ 0 steps; we write µ ⇒ * ρ if there is any finite sequence of reductions from µ to ρ.
With a slight abuse of notation, in the rest of the paper we sometime write {a} for {a 1 }, or simply a when clear from the context. As an example, we write a ⇒ µ for {a 1 } ⇒ µ. Moreover, the distribution {a p 1 1 , . . . , a pn n } will be often indicated as pi · {ai} thus facilitating algebraic manipulations.

Normalization and Confluence
In this subsection, we look at normalization and confluence in the probabilistic setting, which we introduced in Sec. 2.1. We need to distinguish between weak and strong normalization. The former refers to the possibility to reach normal forms following any reduction order, while the latter (also known as termination, see [40]) refers to the necessity of reaching normal forms. In both cases, the concept is inherently quantitative.
Definition 4 (Weak and Strong Normalization). Let p ∈ [0, 1] and let µ ∈ DST (A) Then: • µ weakly p-normalizes (or weakly normalizes with probability at least p) if there exists ρ such that µ ⇒ * ρ and T (ρ) ≥ p. • µ strongly p-normalizes (or strongly normalizes with probability at least p) if there exists n such that µ ⇒ n ρ implies T (ρ) ≥ p, for all ρ. The relation → is said uniform if for each p, and each µ ∈ DST (A), weak p-normalization implies strong p-normalization.
Following [40], we will also use the term p-termination for strong p-normalization, and refer to weak p-normalization as simply p-normalization.
Observe that for every µ there is a unique probability p such that µ ⇓p. Please also observe how Definition 5 is taken over all ρ such that µ ⇒ * ρ, thus being forced to take into account all possible reduction orders. If → is uniform, however, we can reach the limit along any reduction order: Proposition 6. Assume → is uniform. Then for every µ such that µ ⇓p and for every sequence of distributions (ρn)n such that µ = ρ0 and ρn ⇒ ρn+1 for every n, it holds that p = limn→∞ T (ρn).
A PARS is said to be confluent iff ⇒ is a confluent relation in the usual sense: Definition 8 (Confluence). The PARS (A, →) is said to be confluent if whenever τ ⇒ * µ and τ ⇒ * ξ, there exists ρ such that µ ⇒ * ρ and ξ ⇒ * ρ.

The Diamond Property in a Probabilistic Scenario
In this section we study a property which guarantees confluence and uniformity.
Proof. First note that (2) follows from (1). In order to prove (1), we use an adaptation of the familiar "tiling" argument. It is not exactly the standard proof because reaching some normal forms in a distribution is not the end of a sequence of reductions. Assume If k = 1, the claim is true by Definition 9 (1). If k > 1 we tile (w.r.t. ⇒), as depicted below: (2), from ρi ⇒ ρi+1 and ρi ⇒ σi, by closing the diamond. By Defini-

Memory Structures
In this section we introduce the notion of memory structure. Commutativity of the memory operations is ensured by a set of equations.
To deal with the notion of fresh addresses, and avoid unnecessary bureaucracy, it is convenient to rely on nominal sets. The basic definitions are recalled below (for details, see, e.g., [41]).

Nominal Sets
If G is a group, then a G-set (M, ·) is a set M equipped with an action of G on M , i.e. a binary operation (·) : G × M −→ M which respects the group operation. Let I be a countably infinite set; let M be a set equipped with an action of the group Perm(I) of A nominal set is a Perm(I)-set all of whose elements have finite support. In this case, if m ∈ M , we write supp(m) for the smallest support of m. The complementary notion of support is freshness: We write (i j) for the transposition which swaps i and j.
We will make use of the following characterization of support in terms of transpositions: A ⊆ I supports m ∈ M if and only if for every i, j ∈ I − A it holds that (i j) · m = m. As a consequence, for all i, j ∈ I, if they are fresh for m ∈ M then (i j) · m = m.

Memory Structures
A memory structure Mem = (Mem, I, ·, L) consists of an infinite, countable set I whose elements i, j, k, . . . we call addresses, a nominal set (Mem, ·) each of whose elements we call memory states, or more shortly, memories, and a finite set L of operations.
We write I * for the set of all tuples made from elements of I. A tuple is denoted with (i1, . . . , in), or with i. To a memory structure are associated the following maps.
• test : I × Mem → DST (Bool × Mem) (Observe that the set Mem might be updated by the operation test: for this reason, it also appears in the codomain -See Remark 15), Mem (partial map), • arity : L → N, and the following three properties.
(1) The maps test and update respect the group action: , where the action of Perm(I) is extended in the natural way to distributions and pairing with booleans.
(2) The action of a given operation on the memory is only defined for the correct arity. More precisely, update((i1 . . . in), x, m) is defined if and only if the i k 's are pairwise disjoint and arity(x) = n.
(followed by) (followed by) (followed by) (followed by) Figure 1. Commutation of Tests and Updates.
(3) Disjoint tests and updates commute: assume that i = j, that j does not meet k, and that k and k are disjoint. First, updates on k and k commute: update( k, x, update( k , x , m)) = update( k , x , update( k, x, m)). Then, tests on i commute with tests on j and tests of j commute with updates on k. We pictorially represent these equations in Fig. 1. The drawings are meant to be read from top to bottom and represent the successive memories along action. Probabilistic behavior is represented with two exiting arrows, annotated with their respective probability of occurrence, and the boolean resulting from the test operation. Intermediate memories are unnamed and represented with "·". We write the formal equations in Appendix A.

Instances of Memory Structures
The structure of memory is flexible and can accommodate several choice effects. Let us give some relevant examples. Typically, here I is N, but any countable set would do the job.

Deterministic, Integer Registers
The simplest instance of memory structure is the deterministic one, corresponding to the case of classical PCF (this subsumes, in particular, the case studied in [28]). Memories are simply functions m from I to N, of value 0 apart for a finite subset of I. The test on address i is deterministic, and tests whether m(i) is zero or not. Operations in L may include the unary predecessor and successor, and for example the binary max operator. Remark 13. The equations on memory structures enforce the fact that all fresh addresses (i.e., not on the support of the nominal set) have equal values. Note that however the conditions do not impose any particular "default" value. These equations also state that, in the deterministic case, a test action on i can only modify the memory at address i. Otherwise, it could for example break the commutativity of update and test (unless L contains trivial operations, only).

Probabilistic, Boolean Registers
When the test operator is allowed to have a genuinely probabilistic behavior, the memory model supports the representation of probabilistic boolean registers. In this case, a memory m is a function from I to the real interval [0, 1], whose values represent probabilities of observing "true". The test on address i could return Operations in L may for example include a unary "coin flipping" operation setting the value associated to i to some fixed probability.
Example 14. If as in Example 12 we represent the memory as a sequence, a memory filled with the value "false" would be m0 = (0, 0, 0, . . .). Assume c is the unary operation placing a fair coin at the corresponding address; if m1 is update(0, c, m0),

Quantum Registers
A standard model for quantum computation is the QRAM model: quantum data is stored in a memory seen as a list of (quantum) registers, each one holding a qubit which can be acted upon. The model supports three main operations: creation of a new register, measurement of a register, and application of unitary gates on one or more registers, depending on the arity of the gate under scrutiny. This model has been used extensively in the context of quantum lambda-calculi [11,13,24], with minor variations. The main choice to be made is whether measurement is destructive (i.e., if one uses garbage collection) or not (i.e., the register is not reclaimed).
A Canonical Presentation of Quantum Memory. To fix things, we shall concentrate on the presentation given in [13]. We briefly recall it. Given n qubits, a memory is a normalized vector in (C 2 ) ⊗n (equivalent to a ray). A linking function maps the position of each qubit in the list to some pointer name. The creation of a new qubit turns the memory φ ∈ ( Finally, the application of a k-ary unitary gate U on φ ∈ (C 2 ) ⊗n simply applies the unitary matrix corresponding to U on the vector φ. The language comes with a chosen set U of such gates.
Quantum Memory as a Nominal Set. The quantum memory can be equivalently presented using a memory structure: in the following we shall refer to it as Q. The idea is to use nominal set to make precise the hand-waved "pointer name", and formalize the idea of having a finite core of "in use" qubits, together with an infinite pool of fresh qubits. Let F0 be the set of (set-)maps from I (the infinite, countable set of Sec. 3.2) to {0, 1} that have value 0 everywhere except for a finite subset of I. We have a memory structure as follows.
I is the domain of the set-maps in F0. The nominal set (Mem, ·) is defined with Mem = H0, i.e. the Hilbert space built from finite (complex) linear combinations over F0, while the group action (·) corresponds to permutation of addresses: σ · m is simply the function-composition of σ with the elements of F0 in superposition in m. The support of a particular memory m is finite: it consists of the set of addresses that are not mapped to 0 by some (set)-function in the superposition. The set of operations L is the chosen set U of unitary gates. The arity is the arity of the corresponding gate.
Finally, the update and test operations correspond respectively to the application of an unitary gate, and to a measurement followed by a (classical) boolean test on the result. We omit the formalization of these operations in the nominal set setting; instead we show how this presentation in terms of nominal sets is equivalent to the previous more canonical one.
Equivalence of the Two Presentations. Let m ∈ Q. We can always consider a finite subset of I, say I0 = {i0 . . . in} for some integer n such that all other addresses are fresh. As fresh values are 0 in m, then m is a superposition of sequences that are equal to 0 on I \ I0. Then m can be represented as "φ ⊗ |000 . . . " for some (finite) vector φ. We can omit the last |0000 . . . and only work with the vector φ: we are back to the canonical presentation of quantum memory. Update and test can then be defined on the nominal set presentation through this equivalence.
Equations. Memory structures come with equations, which are indeed satisfied by quantum memories. Referring to Sec.

Overview of the Forthcoming Sections
We use memory structures to encapsulate effects in three different settings. In Sec. 4, we enrich proof nets with a memory, in Sec. 5, we enrich token machines with a memory, while in Sec. 6, we equip PCF terms with a memory. The construction is uniform for all the three systems, to which we refer as operational systems, as opposite to the base rewrite systems on top of which we build (see Sec. 1.3).

Program Nets and Their Dynamics
In this section, we introduce program nets. The base rewrite system on which they are built is a variation 1 of SMEYLL nets, as introduced in [28]. SMEYLL nets are MELL (Multiplicative Exponential Linear Logic) proof nets extended with fixpoints (Y-boxes) which model recursion, additive boxes (⊥-boxes) which capture the ifthen-else construct, and a family of sync nodes, introducing explicit synchronization points in the net.
The novelty of this section is the operational system which we introduce in Sec. 4.3, by means of our parametric construction: given a memory structure and SMEYLL nets, we define program nets and their reduction. We prove that program nets are a PARS which satisfies the diamond property, and therefore confluence and uniqueness of normal forms both hold. Program nets also satisfy cut elimination, i.e. deadlock-freeness of nets rewriting.

Formulas
The language of formulas is the same as for MELL. In this paper, we restrict our attention to the constant-only fragment, i.e.: The constants 1, ⊥ are the units. As usual, linear negation (·) ⊥ is extended into an involution on all formulas: Positive formulas P and negative formulas N are respectively defined as: P ::= 1 | P ⊗ P , and N ::= ⊥ | N`N . Figure 3. Boxes.

SMEYLL Nets
A SMEYLL net is a pre-net (i.e. a well-typed graph) which fulfills a correctness criterion.
Pre-Nets. A pre-net is a labeled directed graph R built over the alphabet of nodes represented in Fig. 2.
Edges. Every edge in R is labeled with a formula; the label of an edge is called its type. We call those edges represented below (resp. above) a node symbol conclusions (resp. premises) of the node. We will often say that a node "has a conclusion (premise) A" as shortcut for "has a conclusion (premise) of type A". When we need more precision, we explicitly distinguish an edge and its type and we use variables such as e, f for the edges. Each edge is a conclusion of exactly one node and is a premise of at most one node. Edges which are not premises of any node are called the conclusions of the net.
Nodes. The sort of each node induces constraints on the number and the labels of its premises and conclusions. The constraints are graphically shown in Fig. 2. A sync node has n ∈ N premises of types P1, P2, · · · , Pn respectively and n conclusions of the same types P1, P2, · · · , Pn as the premises, where each Pi is a positive type. A sync node with n premises and conclusions is drawn as n many black squares connected by a line as in the figure. The total number of 1's in the Pi's is called the arity of the sync node. We call boxes the nodes ⊥, !, and Y . The leftmost conclusion of a box is said to be principal, while the other ones are auxiliary. The node ⊥ has conclusion {⊥, Γ} with Γ = ∅. The exponential boxes ! and Y have conclusions {!A, ?Γ} (Γ possibly empty). To each !-box (resp. Y -box) is associated a content, i.e. a pre-net of conclusions {A, ?Γ} (resp. {A, ?A ⊥ , ?Γ}). To each ⊥-box are associated a left and a right content: each content is a pair (bot, S), where bot is a new node that has no premise and one conclusion ⊥, and S is a pre-net of conclusions Γ. We represent a box b and its content(s) as in Fig. 3. The nodes and edges in the content are said to be inside b. As is standard, we often call a crossing of the box border a door, which we treat as a node. We then speak of premises and conclusion of the principal (resp. auxiliary) door. Observe that in the case of ⊥-box, the principal door has a left and a right premise. Depth. A node occurs at depth 0 or on the surface in the pre-net R if it is a node of R. It occurs at depth n + 1 in R if it occurs at depth n in a pre-net associated to a box of R.
Nets. A net is given by a pre-net R which satisfies the correctness criterion of [28], together with a total map mknameR : SyncNode(R) → L, where L is a finite set of names and SyncNode(R) is the set of sync nodes appearing in R (including  those inside boxes); the map mknameR is simply naming the sync nodes. From now on, we write R for the triple (R, L, mknameR). Correctness is defined by means of switching paths. A switching path in the pre-net R is an undirected path on the graph R (i.e. R is regarded as an undirected graph) which uses at most one of the two premisses for each`and ?c node, and at most one of conclusions for each sync node. A pre-net is correct if none of its switching paths is cyclic, and the content of each of its box is itself correct.
Reduction Rules. Fig. 4 describes the rewriting rules on nets. Note that the redex in the top row has two possible reduction rules, u0 and u1. Note also the y reduction, which captures the recursive behavior of the Y -box as a fixpoint (we illustrate this in the example below.) The metavariables X, X1, X2 of Fig. 4 range over {!, Y } and are used to uniformly specify reduction rules involving exponential boxes (i.e., X's can be either ! or Y ). The reduction of net has two constraints: (1.) surface reduction, i.e. a reduction step applies only when the redex is at depth 0, and (2.) exponential steps are closed, i.e. they only take place when the !A premise of the cut is the principal conclusion of a box with no auxiliary conclusion. We come back on the former in Sec. 7.1.2.
As expected, the net reduction preserves correctness.
Example. The "skeleton" of the program in Example 3 could be encoded 2 as in the LHS of Fig. 5. The recursive function f is represented with a Y-box, and has type !(1 1) = !(⊥`1). The test is encoded with a ⊥-box: in one case we forget the function f by using ?w and simply return a one node, and in the other case we apply a Hadamard gate, which is represented with a (unary) sync node. To the "in" part of the let-rec corresponds the dereliction node ?d, triggering reduction. With the rules presented in the previous paragraph, the net rewrites according to Fig. 5  been unwound once. From there, we could reduce the one node with the sync node H, but of course doing so we would not handle the quantum memory. In order to associate to reductions an action on the memory, we need a bit more, namely the notion of a program net which is introduced in Sec. 4.3.

Program Nets
Let Inputs(R) be the set of all occurrences of 1's which are conclusions of one nodes at the surface, and of all the occurrences of ⊥'s which appear in the conclusions of R.
Definition 16 (Program Nets). Given a memory structure Mem = (Mem, I, L), a raw program net on Mem is a tuple (R, indR, m) such that • R is a SMEYLL net (with mknameR : SyncNode(R) → L), • indR : Inputs(R) I is an injective partial map that is however total on the occurrences of ⊥, • m ∈ Mem. We require that the arity of each sync node s matches the arity of mknameR(s). Please observe that in the second item in Definition 16, the occurrences of 1 s belonging to Inputs(R) are not necessarily in the domain of indR; if they are, we say that the corresponding one node is active. Program nets are the equivalence class of raw program nets over permutation of the indexes. Formally, let σ(R, indR, m) = (R, σ · indR, σ · m), for σ ∈ Perm(I). The equivalence class R = [(R, indR, m)] is {σ(R, indR, m) | σ ∈ Perm(I)}. We use the symbol ∼ for the equivalence relation on raw program nets. N indicates the set of program nets.
Reduction Rules. We define a relation ⊆ N × DST (N ), making program nets into a PARS. We first define the relation over raw program nets. Fig. 6 summarizes the reductions in a graphical way; the function indR is represented by the dotted lines.  where l is the label of s, and i are the addresses of its premises. 3. Test. If R u 0 R0 and R u 1 R1, and i is the address of the premise 1 of the cut, then (R, indR, m) where indR 0 (resp. indR 1 ) is the restriction of indR to Inputs(R0) (resp. Inputs(R1)). 4. Otherwise, if R x R with x ∈ {s, u0, u1}, then we have

observe that none of these rules modify the domain of indR).
The relation extends immediately to program nets (by slight abuse of notation we use the same symbol); Lem. 17 guarantees that the relation is well defined. We write (R, indR, m) r µ for the reduction of the redex r in the raw program net (R, indR, m).

Proof. Let us check the rule test
and p i = pi for i ∈ {0, 1}. The first two follow by definition of test(i) and the last two follow from the equation σ·(test(i, m)) = test(σ(i), σ · m). The other rules can be similarly checked.

Remark 18. In the definition of the reduction rules:
• Link is independent from the choice of i. If we chose another address j with the same conditions, then we would have gone to (R, indR ∪ {x → j}, m). However this does not cause a problem: by using a permutation σ = (i j), since σ·m = m we have σ(R, indR ∪ {x → i}, m) = (R, indR ∪ {x → j}, m) and therefore (R, indR ∪ {x → i}, m) and (R, indR ∪ {x → j}, m) are as expected the exact same program net. • In the rules Update and Test, the involved one nodes are required to be active.
The pair (N , ) forms a PARS. Reduction can happen at different places in a net, however the diamond property allows us to deal with this seamlessly. The following two results can be obtained as adaptations of similar ones in [28].
Theorem 21 (Deadlock-Freeness of Net Reduction). Let R = [(R, indR, m)] be a program net such that no ⊥, ? or ! appears in the conclusions of the net R. If R contains cuts, a reduction step is always possible.
Corollary 22 (Cut Elimination). With the same hypothesis as above, if R , (i.e. no further reduction is possible) then R is cut free.
Example. The net in LHS of Fig. 5 can be embedded into a program net with a quantum memory of empty support: (0, 0, 0, . . .) ≡ "|000 . . . ". It reduces according to Fig. 5, with the same memory. The next step requires a link -rewrite step to attach a fresh addresssay, 0-to the one node at surface. The H-sync node then rewrites with a update -step, and we get the program net (A) in Fig. 7 with the "update" action applied to the memory: the memory corresponds to √ 2 2 (|0 + |1 ) ⊗ |00 . . . . From there, a choice reduction is in order: it uses the "test" action of the memory structure, which, according to Sec. 3.3.3 corresponds to the measurement of the qubit at address 0. This yields the probabilistic superposition of the program nets (B1) and (B2). As the net in (B1) is the LHS of Fig. 5, it reduces to (C1) (dashed arrow (a)), similar to (A) modulo the fact that the address 0 was not fresh: the link -rewrite step cannot yield 0: here we choose 1. Note that we could have chosen any other non-zero number as the address. The program net (B2) rewrites to (C2) (dashed arrow (b)): the weakening node erases the Y-box, and a fresh variable is allocated. In this case, the address 0 is indeed fresh and can be picked.

A Memory-Based Abstract Machine
In this section we introduce a class of memory-based token machines, called the MSIAM (Memory-based Synchronous Interaction Abstract Machine). The base rewrite system on which the MSIAM is built, is a variation 3 of the SIAM multi-token machine from [28], which we recall in Sec. 5.1. The specificity of the SIAM is to allow not only parallel threads, but also interaction among them, i.e. synchronization. Synchronization happens in particular at the sync nodes (unsurprisingly, as these are nodes introduced with this purpose), but also on the additive boxes (the ⊥-box). The transitions at the ⊥-box model choice: as we see below, when the flow of computation reaches the ⊥-box (i.e. the tokens reach the auxiliary doors), it continues on one of the two sub-components, depending on the tokens which are positioned at the principal door.
The original contribution of this section is contained in Sections 5.2 through 5.4, where we use our parametric construction to define the MSIAM M R for R as a PARS consisting of a set of states S, and a transition relation → ⊂ S × DST (S), and establish its main properties, in particular Deadlock-Freeness (Th. 26), Invariance (Th. 27) and Adequacy (Th. 28).

SIAM
Let R be a net. The SIAM for R is given by a set of states and a transition relation on states. Most of the definitions are standard. 3 In this paper we make this transition non-deterministic; otherwise there is no major difference. A state is initial if T ⊆ INITR and orig is the identity. We indicate the (unique) initial state of MR by IR. A state T is final if all positions in T belong to either FINR or STABLER.
With a slight abuse of notation, we will denote the state (T, orig) also by T . Given a state T of MR, we say that there is a token in p if p ∈ T . We use expressions such as "a token moves", "crosses a node", in the intuitive way.
SIAM Transitions. The transition rules of the SIAM are described in Fig. 8 and 9. Rules (i)-(iv) require synchronization among different tokens; this is expressed by specific multi-token conditions which we discuss in the next paragraph. First, we explain the graphical conventions and give an overview of the rules.
The position p = (e, s, t) is represented graphically by marking the edge e with a bullet •, and writing the stacks (s, t). A transition T → U is given by depicting only the positions in which T and U differ. It is intended that all positions of T which do not explicitly (and similarly for the right premiss) ( σ, τ .s, t) ? appear in the picture also belong to U . To save space, in Fig. 9 the transition arrows are annotated with a direction; this means that the rule applies (only) to positions which have that direction. When useful, the direction of a position is directly annotated with ↓ , ↑ or ↔ . Note that no transition is defined for stable positions. For boxes, whenever a token is on a conclusion of a box, it can move into that box (graphically, the token "crosses" the border of the box) and it is modified as if it were crossing a node. For exponential boxes, Fig. 9 depicts only the border of the box. We do not explicitly give the function orig, which is immediate to reconstruct when keeping in mind that it is a pointer to the origin of the token. We briefly discuss the most interesting transitions (we refer to [28] for a broader discussion). Fixpoints: the recursive behavior of Yboxes is captured by the exponential signature in the form y(·, ·), and the associated transitions. Duplication: the key is rule (iv), which generates a token on the conclusion of a ?d node; this token will then travel the net, possibly crossing a number of contractions, until it finds its exponential box; intuitively, each such token corresponds to a copy of a box. One: the behavior of the token generated by rule (iii) on the conclusion of a one node is similar to that of a dereliction token; the one token searches for its ⊥-box. Stable tokens: when the token from an instance of a ?d or of a one node "has found its box", i.e. it reaches the principal door of a box, the token become stable (↔). A stable token is akin to a marker sitting on the principal door of its box, keeping track of the box copies and of the choice made in each specific copy.
Multi-token Conditions. The rules marked by (i), (ii), (iii), and (iv) in Fig. 9 require the tokens to interact, which is formalized by multi-token conditions. Such conditions allow, in particular, to capture choice and synchronization. Below we give an intuitive presentation; we refer to [28,42] for the formal details. For convenience we also recall them in Appendix C.
Synchronization, rule (i). To cross a sync node l, all the positions on the premises of l (for the same box stack t) must be filled; intuitively, having the same t, means that the positions all belong to the same copy of l. Only when all the tokens have reached l, they can cross it; they do so simultaneously.
Choice, rule (ii). Any token arriving at a ⊥-box on an auxiliary door must wait for a token on the principal door to have made a choice for either of the two contents, S0 or S1: a token (e, s, t) on the conclusions Γ of the ⊥-box will move to S0 (resp. S1) only if the principal door of S0 (resp. S1) has a token with the same t.
The rules marked by (iii) and (iv) also carry a multi-token condition, but in a more subtle way: a token is enabled to start its journey on a one or ?d node only when its box has been opened; this reflects in the SIAM the constraint of surface reduction of nets.

MSIAM
Similarly to what we have done for nets, we enrich the machine with a memory, and use the SIAM and the operations on the memory to define a PARS. → U (Fig. 9), and let n be the one node, x its conclusion, and p the new token in U . We set where we choose i = indR(x) if the one node is active, and otherwise an address i which is fresh for both indT and (m).

Update. Assume T (i)
→ U (Fig. 9), l is the name associated to the sync node, and i are the addresses which are associated to its premises (by composing orig and ind), then (Fig. 8, non-deterministic transition). If p ∈ T is the token appearing in the redex (Fig. 8), and i the addresses that indT associates to orig(p), then In the next sections, we study the properties of the machine, and show that the MSIAM is a computational model for N .  In Panel (B0): the left-side of the ⊥-box is opened and its onenode emits the token (c) that eventually reaches the conclusion of the net. In Panel (B1): the right-side of the ⊥-box is opened and tokens (c) and (d) are emitted. Token (d) opens a new copy of the Y -box, while token (c) hits the ⊥-box of this second copy. The test action of the memory again spawns a probabilistic distribution.
We focus on panel (C10) on the case of the opening of the leftside of the ⊥-box: there, a new token (e) is generated. It will exit the second copy of the Y -box, go through the first copy and exit to the conclusion of the net.

MSIAM Properties, and Deadlock-Freeness
Intuitively, a run of the machine M R is the result of composing transitions of M R , starting from the initial state I R (composition being transitive composition). We are not interested in the actual order in which the transitions are performed in the various components of a distribution of states. Instead, we are interested in knowing which distributions of states are reached from the initial state. This notion is captured well by the relation (see Sec. 2.1). We will say that a run of the machine M R reaches µ ∈ DST (S R ) if I R µ. We will also use the expression "a run of M R reaches a state T" if I µ with T ∈ SUPP (µ). An analysis similar to the one done for program nets shows the next lemma (Lem. 24) and therefore Prop. 25: Lemma 24 (Diamond). The relation → satisfies the diamond property.
Proposition 25 (Confluence, Uniqueness of Normal Forms, Uniformity). The relation → satisfies confluence, uniformity, and uniqueness of normal forms.
By the results we have studied in Sec. 2, we thus conclude that all runs of M R have the same behavior with respect to the degree of termination, i.e. if I R p-normalizes following a certain sequence of reductions, it will do so whatever sequence of reductions we pick. We say that the machine M R p-terminates if I R p-terminates (see Def. 4).

Deadlocks. A terminal state T
of M R can be final or not. A non-final terminal state is called a deadlocked state. Because of the inter-dependencies among tokens given by the multi-token conditions, a multi-token machine is likely to have deadlocks. We are however able to guarantee that any MSIAM machine is deadlockfree, whatever is the choice for the memory structure.
Theorem 26 (Deadlock-Freeness of the MSIAM). Let R be a program net of conclusion 1; if I R µ and T ∈ SUPP (µ) is terminal, then T is a final state.
The proof (see Appendix D.3) relies on the diamond property of the machine (more precisely, uniqueness of the normal forms).

Invariance and Adequacy
The machine M R gives a computational semantics to R. The semantics is invariant under reduction (Th. 27); the adequacy result (Th. 28) relates convergence of the machine and convergence of the nets. We define the convergence of the machine as the convergence of its initial state: The proofs of invariance and adequacy, are both based on the diamond property of the machine, and on a map-which we call transformation-which allows us to relate the rewriting of program nets with the MSIAM. To obtain the proofs, we need to establish a series of technical results which we give in Appendix D.

A PCF-style Language with Memory Structure
We introduce a PCF-style language which is equipped with a memory structure, and is therefore parametric on it. The base type will correspond to elements stored in the memory, and the base operations to the operations of the memory structure.

Syntax and Typing Judgments
The language PCF LL which we propose is based on Linear Logic, and is parameterized by a choice of a memory structure Mem.
The terms (M, N, P ) and types (A, B) are defined as follows: M, N, P : where c ranges over the set of memory operations L. A typing context ∆ is a (finite) set of typed variables {x1 : A1, . . . , xn : An}, and a typing judgment is written as ∆ M : A. An empty typing context is denoted by "·". We say that a type is linear if it is not of the form !A. We denote by !∆ a typing context with only non-linearly typed variables. A typing judgment is valid if it can be derived from the set of typing rules presented in Fig. 11. We require M and N to have empty context in the typing rule of if P then M else N . The requirement does not reduce expressivity as typing contexts can always be lambda-abstracted. The typing rules make use of a notion of values, defined as follows: U, V ::= x | λx.M | U, V | c.

Operational Semantics
The operational semantics for PCF LL is similar to the one of [13], and is inherently call-by-value. Indeed, being based on Linear Logic,

Modeling PCF LL with Nets
We now encode PCF LL typing judgments and typed PCF AM closures into program nets. As the type system is built on top of Linear Logic, the translation (−) † is rather straightforward, modulo one subtlety: it is parameterized by a memory structure m and a partial function ind mapping term variables to addresses in I.

Results and Discussion
As we anticipated in Sec. 1.3, we have proved-parametrically on the memory-that the MSIAM is an adequate model of program nets reduction (Th. 28), and program nets are expressive enough to adequately represent the behavior of the PCF LL abstract machine (Th. 29). What does this mean? As soon as we choose a concrete instance of memory structure, we have a language and an adequacy result for it. This is in particular the case for all instances of memory which are outlined in Sec. 3.3. To make this explicit, let I, P and Q be respectively a deterministic, probabilistic and quantum memory. We denote by PCF LL (I), PCF LL (P) and PCF LL (Q), respectively, the language which is obtained by choosing that memory. Observe in particular that the choice of P or Q, respectively specialize our adequacy result into a semantics for a probabilistic PCF in the style of [33], and a semantics for a quantum PCF, in the style of [11,13].

The Quantum Lambda Calculus
Let us now focus on the quantum case, and analyze in some depth our result. We have a quantum lambda-calculus, namely PCF LL (Q), together with an adequate multi-token semantics. How does our calculus relate with the ones in the literature?
We first observe that the syntax of PCF LL (Q) is very close to the language of [13] (we only omit lists and coproducts). The operational semantics is also the same, as one can easily see. Indeed, the abstract machine in [13] consists of a triple (Q, L, M ) where M is a lambda-term and where Q and L are as presented in Sec. 3.3.3. As we discussed there, for Q and L one can use either the canonical presentation of [13], or the memory structure Q.

Discussion on the Quantum Model
It is now time to go back to the programs in our motivating examples, Examples 2 and 3. Both programs are valid terms in PCF LL (Q); we have already informally developed Example 3 within our model.
We claimed in the Introduction that Example 2 cannot be represented in the GoI model described in [21]: the reason is that the model does not support entangled qubits in the type α⊗α (using our notation), a tensor product is always separable. To handle entangled states, [21] uses non-splittable, crafted types: this is why the simple term in Example 2 is forbidden. In the MSIAM, entangled states pose no problem, as the memory is disconnected from the types.
The term of Example 3, valid in PCF LL (Q), is mapped through (−) † to the net of Fig. 5: Th. 29 and 28 state that the corresponding MSIAM presented in Fig. 10 is adequate. Note that Example 3 was presented in the context of quantum computation. It is however possible (and the behavior is going to be the same as the one already described) to use the probabilistic memory sketched in Sec. 3.3.2. In this case, the H-sync node would be changed for the coin-sync node.

Qubits, Duplication and Erasing
It is worth to pinpoint the technical ingredients which allow for the coexistence of quantum bits with duplication and erasing. In the language, the reason is that, similarly to [13], PCF LL allows only lambda-abstractions (or tuples thereof) to be duplicated. In the case of the nets (and therefore of the MSIAM), the key ingredient is surface reduction (Sec. 4.2): the allocation of a quantum bit is captured by the link rule which associates a one node to the memory. Since a one node linked to the memory cannot lie inside a box, it will never be copied nor erased. Indeed, the ways in which the language and the model deal with quantum bits, actually match.

More Possibilities for Quantum Memory Structure
In the presentation of Q we have given in Sec. 3.3.3, fresh qubits were arbitrarily created in state |0 . We could as well have chosen, say, |1 for default value. Formally, if we want to do that we can use the set F1 of (set-)maps from I to {0, 1} that have value 1 everywhere except for a finite subset of I. The structure Q would then have been defined as H1, the Hilbert space built from finite linear combinations of F1.
Unlike the case of the integer memory, the mathematical properties of quantum states can make the test action modify the state of the fresh addresses. Let us see how this happens.
Indeed, one can not only build a memory structure Q with H0 and H1 but also with a superposition of the elements in H0 and H1. For example, one could choose Q = {αv0 + βv1)|vx ∈ Hx, |α| 2 + |β| 2 = 1}. This makes a memory structure satisfying all the equations. In this system, a valid memory can have all of its fresh variables in superposition. Any measurement on a fresh variable of this memory will collapse the state... and "modify" the global state of the fresh variables. So, despite the fact that a test on i cannot touch another address, it can globally act on the memory.
This paradox is of course solved when remembering that measurements and unitary operations (and measurements and measurements) do commute independently of the state on which they are applied (Remark 1). So the fact that the memory changes globally after a test is irrelevant.

Conclusion
In this paper, we have introduced a parallel, multi-token Geometry of Interaction capturing the choice effects with a parametric memory. This way, we are able to represent classical, probabilistic and quantum effects, and adequately model the linearly-typed language PCF LL parameterized by the same memory structure. We expect our approach to capture also non-deterministic choice in a natural way: this is ongoing work.

A. Commutation of Tests and Updates on Memory States
The commutation of tests and updates is formally defined as follows.
Assume that i = j, that j does not meet k, and that k and k are disjoint.
• Tests on i commute with tests on j. More precisely, if

B. Program Nets: proof of the Diamond Property
We prove that the PARS (N , ) satisfies the diamond property (Prop.19 ). We write (R, indR, m) r µ for the reduction of the redex r in the raw program net (R, indR, m).
First, we observe the following property, proven by case analysis.
The proof of Prop. 19 goes as follows.
If r1 and r2 are both non-active one nodes, say x and y respectively, (R, indR, m) reduces to (R, indR ∪ {x → i, y → j}, m) and (R, indR ∪ {x → k, y → l}, m) for some fresh indexes i, j, k, l. The permutation (i, k) • (j, l) renders the two program nets equivalent.
If both r1 and r2 modify memories (i.e. they perform either update or test), the property holds because the injectivity of indR guarantees that we always have the requirement (disjointness of indexes) of the equations given in Appendix A. Hence the two reductions commute both on memory (up to group action) and on probability.

C. SIAM: Multitoken Conditions, Formally
Stable Tokens. A token in a stable position is said to be stable. Each such token is the remains of a token which started its journey from DER or ONES, and flowed in the graph "looking for a box". This stable token therefore witnesses the fact that an instance of dereliction or of one "has found its box". Stable tokens keep track of box copies; let us formalize this. Let S be either R, or a structure associated to a box (at any depth). Given a state T of MR, we define Copies T (S) to be { } if R = S (we are at depth 0). Otherwise, if S is the structure associated to a box node b of R, we define Copies T (S) as the set of all t such that (e, s, t) is a stable token on the premiss(es) of b's principal door. Intuitively, each such t identifies a copy of the box which contains S.
Multitoken Conditions: Synchronization, Choice, and Boxes Management. Rules marked by (i), (ii), and (iii), (iv) in Fig. 9 only apply if the following conditions are satisfied. (i) Tokens cross a sync node l only if for a certain t, there is a token on each position (e, s, t) where e is a premise of l, and s indicates an occurrence of atom in the type of e. In this case, all tokens cross the node simultaneously. Intuitively, insisting on having the same stack t means that the tokens all belong to the same box copy. (ii) A token (e, s, t) on one of the conclusions Γ of the ⊥-box can move inside the box only if its box stack t belongs to Copies T (S0) (resp. Copies T (S1)), where S0 (resp. S1) is the left (resp. right) content of the ⊥-box. Note that if the ⊥-box is inside an exponential box, there could be several stable tokens on each premise of the principal door, one stable token for each copy of the box. Intuitively, each (e, , t) (resp. (e, δ, t)) corresponds to a copy of one (resp. ?d) node.

D. MSIAM
The proofs of invariance, adequacy, and deadlock-freeness, all are based on the diamond property of the machine, and on a map-which we call Transformation-which allows us to relate the rewriting of program nets with the MSIAM. In this section we establish the technical tools we need. In Sec. D.2 we prove Invariance, in Sec. D.3 we proof adequacy and deadlock-freeness. The tool we use to relate net rewriting and the MSIAM is a mapping from states of R to states of Ri, which we are going to introduce in this section. This tool together with confluence (due to the diamond property) allows us to establish the main result of this section, from which Invariance (Th. 27) follows.
From now on, we use the following conventions and assumption.
• The letters T , U range over raw MSIAM states, the letters T, U over MSIAM states, and the letters T, U over SIAM states.
• To keep the notation light, we will occasionally rely on our convention of denoting the distribution {T 1 } by {T} or even simply by T, when there is no ambiguity.
• Unique initial state. We assume that R has a single conclusion, which has type 1. As a consequence, Dom(indR) = ONESR, and M R has a a unique raw initial state, which is I R = (∅, ∅, mR). We have I R = {IR}. • We denote by S I R the set of states T which can be reached from I R , i.e. I R µ and T ∈ SUPP (µ).
• we do not insist too much on the distinction between raw states and states, which in this section is not relevant.

D.1 Properties and Tools
In this section, most of the time we analyze the reduction of raw program nets and raw states, because we do not need to use the equivalence relation. Which is the same: we pick a representative of the class, and follow it through its reductions.

D.1.1 Exploit the Diamond
Because the MSIAM is diamond, we can always pick a run of the machine which is convenient for us to analyze the machine. By confluence and uniqueness of normal forms, all choices produce the same result w.r.t. both the degree of termination of any distribution which can be reached (invariance), and the states which are reached (deadlock-freeness).
In case of R ρ via link, update or test, we will always choose a run which begins as indicated below: The machine does the same: from the initial state the machine transitions using its reduction link(n, j), on the same one node. We can choose the same address j because we know it is fresh for mR. Therefore we have (I, indI , mR) → link(n,j) {(R , indR, update(l, i, mR)}. Observe that the one node n in the redex is active; let j be the corresponding address. We choose a run which starts with the transitions (I, indI , mR) → link(n,j) {(U, indU , mR)} and (U, indU , mR) → update(s) {(U, indU , update(l, i, mR)} = µ. 3. Test. Assume (R, indR, mR) test(j) ρ where for each i, R u i Ri. Again the one node n in the redex is active; let j be the corresponding address. Our canonical way to start the run of the machine applies to the initial state (I, indI , mR) the transition link(n, j), crosses the cut, and finally applies the same test(j), to reach test(j, mR)[true := U0, false := U1]) = µ.

D.1.2 The Transformation Map
The tool we use to relate net rewriting and the MSIAM is a mapping from states of M R to states of M R i . We first define a map on positions of R, then on SIAM states, and finally on MSIAM raw states.
Transformation of SIAM States. For each Ri to which R reduces, we define a transformation on positions, as a partial function trsfR R i : POSR POSR i . The key case is the case of ⊥-box reduction, illustrated in Fig. 13; for each position outside the redex, we intend that trsf(p) is the identity. The other cases are as in [28].
The definition extends to the states of the SIAM point-wisely, in the obvious way.
From now on, we write trsfR i or sometimes simply trsfi for trsfR R i .
Transformation of MSIAM States. We now extend trsfR R i to MSIAM states. To do so smoothly, we define a subset [trsfR i ] of S I R , which depends on the reduction rule. To work with such states simplify the proofs, and is always possible because of Sec. D.1.1.
• Case link(n,j) . We define [trsfR i ] as the set of the states in S I R in which ind(p) = j, where p is the position associated to the one node n.
• Case update(s) . We define [trsfR i ] as the set of the states in S I R which "have crossed" the sync node s. We can easily characterize these states. Assume p1, . . . , pn are the positions associated to the premises of s (observe that each pi belongs to ONESR). [trsfR i ] is the set of the states T ∈ S I R such that {p1, . . . , pn} ⊆ orig(T ) and {p1, . . . , pn} ⊆ T . • Case test(j) . We define [trsfR 0 ] as the set of the states in S I R which have a token on the left bot of the redex (the edge e0 in the Fig. 13). We define [trsfR 1 ] similarly.

D.1.3 Properties of the Reachable States
Let us analyze the set of states which is spanned by a run of the MSIAM. Given a ⊥-box of R, let e0 be the conclusion of the left ⊥ and e1 be the conclusion of the right ⊥. For any stacks s, t, we call the two stable positions (e0, s, t) and (e1, s, t) a ⊥pair. These two positions are mutually exclusive in a state, because orig(e0, s, t) = orig(e1, s, t).
We say that two states T, U ∈ S I R are in conflict, written T U, if T contains one of the two positions of a ⊥-pair and S the other. We observe that conflict is hereditary with respect to transitions, because stable positions are never deleted or modified by a transition. Let ↑(T) = {U | T ⇒ * ρ ∧ U ∈ SUPP (ρ)}.

.4 The Reachability Relation
The reachability relation (defined in Sec. 2.1) is a useful tool in the study of the MSIAM.
A derivation of a µ is inductively obtained by using the rules which define .
In the case of the MSIAM the relations and ⇒ are equivalent with respect to normal forms. Proof. The former part is by induction on n. The latter is by structural induction (on the rules shown above).
It is helpful to define also another auxiliary relation T • τ which holds if there exists µ satisfying µ and τ ⊆ µ • . This relation 4 states that T reaches a set of terminal states. It is immediate that T • τ iff ∃ρ, T ⇒ * ρ and τ ⊆ ρ • .

D.1.5 Properties of trsf
We now study the action of trsf on transitions. We first look at how trsf maps initial/final/deadlock states. It is also important to understand the action of trsf on the number of stable tokens. We observe that the number of tokens, and stable tokens in particular, in any state T which is reached in a run of MR is finite. We denote by S(T) the number of stable tokens in T. The following is immediate by analyzing the definition of transformation, and checking which tokens are deleted.
Fact 38 (stable tokens). For any trsfR i , S(T) ≥ S(trsfR i (T)). Moreover, if the reduction is d, y or ui, then we also have that S(T) > S(trsfR i (T)).

D.2 Invariance
We prove the following result, from which invariance (Th. 27) follows.
Proposition 39 (Main Property). Assume R i pi · {Ri}. I R q-terminates if and only if I R i qi-terminates and (qi · pi) = q.
Let us first sketch the ingredients of the proof. We need to work our way "back and forth" via Lemmas 42 and 43, because of the following facts.
• Unfortunately, for I R ⇒ * µ it is not true that trsfR i (I R ) ⇒ * trsfR i (µ). However we have that if I R µ in MR, then trsfR i (I R ) trsfR i (µ) (under natural conditions). This is made precise by Lemma 42. • On the other side, the strength of the relation ⇒ is that if I R ⇒ n µ, then for any sequence of the same length I R ⇒ n ρ, we have that ρ • = µ • . This is not the case for the relation which is not informative. The (slightly complex) construction which is given by Lemma 43 allows us to exploit the power of ⇒.