Akira Yoshimizu

Ichiro Hasuo

Claudia Faggian

Ugo Dal

Ugo Dal Lago

Measurements in Proof Nets as Higher-Order Quantum Circuits

teaching and research institutions in France or abroad, or from public or private research centers.

Introduction

Quantum Programming Languages. Quantum computation and quantum communication have been attracting growing attention. The former achieves real breakthrough in computational power-at least for some classes of problems, such as the integer factorization problem (Shor's algorithm) and search problems. While it is often disputed if quantum computation is physically realizable, quantum communication is close to actual deployment in real-world applications. By exploiting the nonlocal character of quantum phenomena (notably quantum entanglement), quantum cryptography protocols accomplish perfect security that do not rely on any computational assumptions (like Diffie-Hellman).

Compared to the algorithmic aspects, the theory of quantum programming is relatively new. For example, quantum algorithms are most often expressed in quantum circuits that lack structuring means like recursion or higher-order functions. Consequently we have seen some proposals for quantum programming languages including QCL [START_REF] Ömer | Quantum programming in QCL[END_REF], quantum lambda calculi [START_REF] Selinger | Quantum lambda calculus[END_REF][START_REF] Van Tonder | A lambda calculus for quantum computation[END_REF] and most recently Quipper [START_REF] Green | Quipper: a scalable quantum programming language[END_REF]: QCL is imperative and the others are functional.

Our interests are in a quantum lambda calculus as a prototype of functional quantum programming languages. The functional style comes with several advantages. For one, a type system based on resource-sensitive linear logic [START_REF] Girard | Linear logic[END_REF] can force no-cloning of quantum states via type safety [START_REF] Van Tonder | A lambda calculus for quantum computation[END_REF]. Moreover, various techniques for classical functional programming can often be "transferred" to the quantum setting, since they are formulated in an abstract mathematical language and hence are generic. For example, in [START_REF] Hasuo | Semantics of higher-order quantum computation via geometry of interaction[END_REF][START_REF] Malherbe | Presheaf models of quantum computation: An outline[END_REF][START_REF] Selinger | Quantum lambda calculus[END_REF] various semantical techniques in the classical setting-such as linearnonlinear adjunctions, categorical geometry of interaction, and presheaf completionare applied to quantum calculi, exploiting the categorical genericity of these techniques.

From Quantum Circuits to Proof Nets. The current work relies on another rich body of techniques that are developed in the linear logic community. Specifically we follow the line of [START_REF] Dal Lago | On multiplicative linear logic, modality and quantum circuits[END_REF][START_REF] Dal Lago | Wave-style token machines and quantum lambda calculi[END_REF] where, roughly speaking, proof nets are thought of as extended quantum circuits.

Proof nets as devised in [START_REF] Girard | Linear logic[END_REF] are a graphical presentation of linear lambda terms (i.e. linear logic proofs) whose principal concern is reduction of terms (i.e. cut-elimination). Proof nets are "extended quantum circuits" in the following sense: (some) wires in proof nets can be naturally identified with those in quantum circuits; and at the same time higher-order computation is naturally accommodated using a linear type system (A ⊸ B ≡ A ⊥ `B). This view is hence a quantum version of the one in [START_REF] Terui | Proof nets and boolean circuits[END_REF]. See §3.5 for further discussion.

Once a quantum lambda term is presented as a proof net, the geometry of interaction (GoI) interpretation [START_REF] Girard | Geometry of interaction 1: Interpretation of system F[END_REF]-especially its concrete presentation as token machines [START_REF] Mackie | The geometry of interaction machine[END_REF]gives a concrete and operational interpretation of the term as a state transition system. This is a main advantage of the current "proof net and GoI" approach compared to the categorical one taken in [START_REF] Hasuo | Semantics of higher-order quantum computation via geometry of interaction[END_REF][START_REF] Malherbe | Presheaf models of quantum computation: An outline[END_REF]: in the latter models tend to be abstract and huge.

A main disadvantage, however, is that it is harder to interpret extra features in a calculus. Such desired features include recursion and accommodation of duplicable classical data by the ! modality; these are all present e.g. in [START_REF] Hasuo | Semantics of higher-order quantum computation via geometry of interaction[END_REF]. In fact, in the preceding work [START_REF] Dal Lago | On multiplicative linear logic, modality and quantum circuits[END_REF][START_REF] Dal Lago | Wave-style token machines and quantum lambda calculi[END_REF] of the current approach, even measurements are excluded from the calculi. Hence important (and basic) examples like quantum teleportation cannot be expressed in their calculi.

Contributions.

In the current work we present a comprehensive framework for programming and interpreting higher-order quantum computation based on a linear lambda calculus, proof nets and GoI interpretation. More specifically:

• We introduce MLLqm, a linear lambda calculus with quantum primitives (including measurement, unlike [START_REF] Dal Lago | On multiplicative linear logic, modality and quantum circuits[END_REF][START_REF] Dal Lago | Wave-style token machines and quantum lambda calculi[END_REF]). • We define a notion of proof net, into which terms of MLLqm are translated. For accommodating measurements we follow the idea of (additive) slices (see e.g. [START_REF] Girard | Proof-nets: The parallel syntax for proof-theory[END_REF]).

We also define the reduction of proof nets and prove that it is strongly normalizing. • We define token machine semantics of MLLqm proof nets and prove that it is sound, i.e., is invariant under reduction of proof nets. Here we have multiple tokens in a token machine (this is as in [START_REF] Dal Lago | Wave-style token machines and quantum lambda calculi[END_REF]); the slices are suitably handled following the token machine semantics in [START_REF] Laurent | A token machine for full geometry of interaction[END_REF] for additives. Our framework attains a balance between expressivity and concreteness of models that we find pleasant. On the one hand, the calculus MLLqm is reasonably expressive: it does include all the quantum operations (preparation, unitary transformation, and most importantly, measurement) and is capable of expressing examples like quantum teleportation, which is not possible in the earlier work [START_REF] Dal Lago | On multiplicative linear logic, modality and quantum circuits[END_REF][START_REF] Dal Lago | Wave-style token machines and quantum lambda calculi[END_REF] of the same proof net approach. Moreover, our framework can naturally express higher-order procedures that are essential e.g. in formalizing quantum pseudo-telepathy games in quantum game theory. The latter are attracting attention as a useful presentation of quantum nonlocality (see e.g. [START_REF] Gisin | Pseudo-telepathy: input cardinality and Bell-type inequalities[END_REF]). On the other hand, while the languages in [START_REF] Hasuo | Semantics of higher-order quantum computation via geometry of interaction[END_REF][START_REF] Malherbe | Presheaf models of quantum computation: An outline[END_REF][START_REF] Selinger | Quantum lambda calculus[END_REF] are much more expressive-they include duplicable classical data (by the ! modality) and/or recursion-their models given in [START_REF] Hasuo | Semantics of higher-order quantum computation via geometry of interaction[END_REF][START_REF] Malherbe | Presheaf models of quantum computation: An outline[END_REF] rely on abstract categorical constructions and it is not trivial to describe them in concrete terms. In contrast, our token machine semantics for MLLqm is given explicitly by a transition system.

The current work shares the same interest as [START_REF] Abramsky | A categorical semantics of quantum protocols[END_REF], in the sense that both aim at pictorial formalisms for operational structures in quantum computation. We follow the linear logic tradition; an advantage is explicit correspondence with a term calculus. In contrast, [START_REF] Abramsky | A categorical semantics of quantum protocols[END_REF] employs string diagrams for monoidal categories (more specifically compact closed categories with biproducts). The two approaches are not unrelated: there is a body of literature studying monoidal categories as models of linear logic. See [START_REF] Melliès | Categorical semantics of linear logic[END_REF] for a survey.

Organization of the Paper. After introducing the calculus MLLqm in §2, in §3 we define MLLqm proof nets and translate terms into proof nets. As usual, proof nets are defined to be proof structures satisfying a certain correctness criterion. We also define reduction (i.e. cut-elimination) of proof nets. In §4 we give GoI semantics to MLLqm proof nets, in the form of token machines. Our main result is soundness of the GoI semantics, i.e. that it is invariant under reduction of proof nets. Quantum teleportation will exemplify these constructions.

Proofs are deferred to Appendix. Familiarity to linear logic techniques like proof nets and token machine semantics is helpful in reading this paper. Our favorite reference is [START_REF] Pinto | Implantation Parallèle avec la Logique Linéaire (Applications des Réseaux d'Interaction et de la Géométrie de l'Interaction[END_REF].

Syntax of Quantum Lambda Calculus MLLqm

We introduce a typed calculus MLLqm. It is a term calculus based on linear logicspecifically multiplicative linear logic (MLL) that has connectives ⊗, `and (•) ⊥ . It is further augmented with quantum primitives that are rich enough to express any quantum operation. The latter notion is roughly for "what we can do to quantum states" and can be represented as a combination of preparation, unitary transformation and measurement. See [START_REF] Nielsen | Quantum Computation and Quantum Information[END_REF]Chap. 8] for more details. The name MLLqm stands for "MLL for quantum computation with measurements." Definition 2.1 (Types of MLLqm) Types of MLLqm are defined by the following BNF:

A, B ::

= qbit | qbit ⊥ | A ⊗ B | A `B .
The syntactic equality shall be denoted by ≡. As is customary in linear logic, we syntactically identify types according to the following rules:

(A ⊗ B) ⊥ ≡ A ⊥ `B⊥ , (A `B) ⊥ ≡ A ⊥ ⊗ B ⊥ , and (A ⊥ ) ⊥ ≡ A. We write A ⊸ B for A ⊥ `B and A ⊗n for (• • • (A ⊗ A) ⊗ A) • • • ) ⊗ A (here ⊗ occurs n -1 times).
= x | λx A .M | M N | M, N | λ x A , y B .M | new |ϕ | U | if meas M then N else L .
Here x is an element of a fixed countable set Var of variables. new |ϕ is a constant for each normalized vector |ϕ in C 2 and designates preparation of a qubit. U is a constant for each 2 n -dimension unitary matrix, where n ∈ N. Measurements meas occur only in conditionals. Note that in variable binders λx A and λ x A , y B , variables x, y come with explicit type labels. This is to ensure Lem. 2.5.

Remark 2.3

The constructor if meas M then N else L is intended for "classical control": operationally, the qubit represented by M is actually measured before going on to evaluate N or L. This is not to be confused with "quantum control." In quantum circuits, it is wellknown that any measurement can be postponed to the end of a circuit (the principle of deferred measurement, [18, §4.4]). This is possible by use of controlled operations like CNOT [18, §4.3]. We shall stick to classical control because, in the current higher-order setting, it is not clear how to simulate classical control by quantum control, or how to systematically construct quantum controlled operations.

x : A ⊢ x : A ax Γ, x : A ⊢ M : B Γ ⊢ λx A .M : A ⊸ B ⊸I1 Γ, x : A, y : B ⊢ M : C Γ ⊢ λ x A , y B .M : A ⊗ B ⊸ C ⊸I2 Γ ⊢ M : A ⊸ B ∆ ⊢ N : A Γ, ∆ ⊢ M N : B ⊸E Γ ⊢ M : A ∆ ⊢ N : B Γ, ∆ ⊢ M, N : A ⊗ B ⊗I ⊢ new |ϕ : qbit new ⊢ U : qbit ⊗n ⊸ qbit ⊗n Un Γ ⊢ M : qbit ∆ ⊢ N : A ∆ ⊢ L : A Γ, ∆ ⊢ if meas M then N else L : A meas
The rule ⊸I 2 replaces the usual ⊗E rule that is problematic in the current linear setting. The following will enable inductive translation of terms into proof nets.

Lemma 2.5 A derivable type judgment Γ ⊢ M : A has a unique derivation.

⊓ ⊔

MLL Proof Nets with Quantum Nodes

In this section we introduce the notion of proof nets tailored for the calculus MLLqm. It is based on MLL proof nets [START_REF] Girard | Linear logic[END_REF] (see also [START_REF] Pinto | Implantation Parallèle avec la Logique Linéaire (Applications des Réseaux d'Interaction et de la Géométrie de l'Interaction[END_REF]) and has additional nodes that correspond to quantum primitives (preparation, unitary transformation and measurement). Among them, (conditionals based on) measurements are the most challenging to model; we follow the idea of additive slices that are successfully utilized e.g. in [START_REF] Mairson | On the computational complexity of cut-elimination in linear logic[END_REF].

As usual, we start with the notion of proof structures as graphs consisting of certain nodes. Then proof nets are defined to be those proof structures which comply with a correctness criterion (like Danos & Regnier's in [START_REF] Danos | The structure of multiplicatives[END_REF]). We define translation of MLLqm terms into proof structures, which we prove to be proof nets. Moreover, we define reduction of proof structures, which we think of as one operational semantics of MLLqm terms. It is shown that proof nets are reduced to proof nets, and that reduction of proof nets is strongly normalizing (SN). Note that recursion is not in MLLqm.

MLLqm Proof Structures

!"! "! "! "! #$!% #! an if node
In addition to the usual nodes in MLL proof nets, we introduce three kinds of nodes for quantum computation: new (preparation of a single qubit), U (unitary transformations/gates), and if (conditionals according to measurement of a qubit). An if node is as shown on the right. It is like a box in standard proof nets.

An if node will appear in a proof structure in the form where the two dashed boxes on its top are filled with "internal" proof structures. Such a combination of an if node and two (internal) proof structures shall be called a meas node. Overall, in MLLqm proof structures we allow the following seven kinds of nodes (Fig. 1). Note that nodes and proof structures are defined by mutual induction: in a proof structure there is a meas node, in whose dashed boxes there are other internal proof structures, and so on. We will make this precise in Def. 3.1. In Fig. 1, a unitary gate node for a 2 n -dimension unitary matrix U has n-many qbit edges and n-many qbit ⊥ edges. Γ denotes a finite sequence of types. In a meas node, the qbit ⊥ -typed edge sticking out to the down-left is called a query edge.

!"! ! "! ! ! #$%! ! "! ! ! #! ! ! & ! ! ! # & ! !! ! ! & ! ! ! ! & !
As usual, incoming edges of a node are called premises and outgoing edges are called conclusions. A proof structure is roughly a graph that consists of nodes in Fig. 1, and is augmented with a quantum state called a quantum register, whose functionality we shall explain by an example.

See Fig. 2. The outermost proof structure (we say it is of level 0) has two new

!"#$% ! ! " "#$%& ! # "#$%' ()* + ! ,! "#$% $! "#$% ! !! "#$% ! ! " "#$% ! -! "#$% $! "#$% ! !! "#$% ! ! " "#$% ! $.! reg: 1 ! reg: 1 ! "#$% ! ! " "#$% ! "#$% $! "#$%' /0%! ()* 1 ! reg: ! $.! !! "#$% $! "#$% ! 23! reg: 1 ! "#$% ! ! " "#$% ! "#$% $! "#$%' /0%! "#$% ! ! " "#$% ! #! ()* 4 ! "#$%' √ 3 2 |03 + 1 2 |13 reg: ! 1 √ 2 |0 1 0 2 + 1 √ 2 |1 1 1 2
Fig. 2: an example of proof structure nodes, a cut node, a ⊗ node and a meas node. Its quantum register is a state of a 2qubit system; each qubit corresponds to a certain new node and the correspondence is designated by indices. Therefore our intention is that each proof structure has a quantum register whose size is the number of new nodes, and that the proof structure explicitly carries the content of the quantum register. Such pairing of computational structure (proof structures here) and quantum registers is inspired by the operational semantics of [START_REF] Selinger | Quantum lambda calculus[END_REF], where a term of a calculus and a quantum state together form a quantum closure.

Definition 3.1 (MLLqm proof structure) Let S be a directed finite graph consisting of nodes in Fig. 1; Q be a quantum register of length n ∈ N (that is, a normalized vector in C 2 n ); k be the number of new nodes in S; and l be a bijection {the new nodes in S} ∼ = → {1, 2, . . . , k}. A triple (S, Q, l) satisfying -each edge in S is well-typed; -no incoming edge in S is dangling; and n = k is called a proof structure. The types on the dangling outgoing edges in S are called the conclusions of S.

Let (S 0 , Q 0 , l 0 ) and (S 1 , Q 1 , l 1 ) be proof structures with the same conclusions, say Γ . We call a triple if node, (S 0 , Q 0 , l 0 ), (S 1 , Q 1 , l 1 ) a meas node and regard it as a node with conclusions qbit ⊥ , Γ . Each of the proof structures (S 0 , Q 0 , l 0 ) and (S 1 , Q 1 , l 1 ) is called a branch of the meas node.

The outermost proof structure is said to be of level 0 and the branches of a meas node of level n are said to be of level n + 1.

We emphasize again that the above definitions of proof structures and meas nodes are mutually inductive. We allow meas nodes nested only finitely many times. The bijection l in a proof structure (S, Q, l) gives indices to new nodes and designates correspondences between new nodes and qubits in a quantum register Q.

For example, in Fig. 2 the unitary gate nodes U and V belong to level 2. The quantum state that corresponds to the node new 3 is in the level-1 register. Note that it is invisible from level 0.

Finally we define slices for MLLqm proof structures, like usual additive slices. We will employ this notion later in §4. Definition 3.2 (Slicing and slices) Let N = (S, Q, l) be an MLLqm proof structure. A slicing is a function b : {all if nodes in S (of any level)} → {0, 1}. Abusing notation, a slice b(N ) is a graph obtained by deleting the unselected branch of each if node according to the slicing b, i.e. if b(v) = 0 delete the branch on the right and if b(v) = 1 delete the branch on the left for each if node v. Note that a slice is not a proof structure.

Reduction of MLLqm Proof Structures

We now introduce reduction rules for MLLqm proof structures. Following the Curry-Howard intuition that normalization of a proof is computation, a reduction step is thought of as a step in quantum computation.

Definition 3.3 (Reduction rules of MLLqm proof structures)

Reduction rules are shown in Fig. 3. The first two are standard in MLL proof nets; the latter three are new. In the unitary gate rule, the unitary matrix U j1,...,jm acts on j 1 , . . . , j m -th qubits in the same way as U does, and leaves other qubits unchanged. The last two rules occur probabilistically, where the resulting quantum registers |ϕ ′ 0 , |ϕ ′ 1 and probabilities j |α j | 2 , j |β j | 2 defined in the obvious way. Explicitly:

|ϕ0 = j αj |ψ 0 j ⊗ |0 ⊗ |χ 0 j , |ϕ ′ 0 = j α j √ k |α k | 2 |ψ 0 j ⊗ |χ 0 j , |ϕ1 = j βj |ψ 1 j ⊗ |1 ⊗ |χ 1 j , |ϕ ′ 1 = j β j √ k |β k | 2 |ψ 1 j ⊗ |χ 1 j , (1)
where |ψ b j of length m -1 and m is the index of the new node that is measured. The other rules occur with probability 1. In meas rules, the indexing function l is suitably updated too.

ax !"! #$%! ! "! ! ! ! ! reg: Q! ! ! reg: Q! ⊗-`! "#! "! !! $ ! % ! $ ! " % ! $ #! % #! $ #! ! % #! reg: Q! !"#! !"#! $ ! % ! $ #! % #! reg: Q! unitary gate reg: Q! !"# $% ! &! '()! !"# $* ! '()! +,-) "! +,-) "! +,-) ! +,-) ! +,-) ! +,-) ! reg: U j1, … jm Q! !"# $% ! !"# $* ! +,-) ! +,-) ! meas0 reg: |φ 0 ! + |φ 1 !" !"#$ " #" !"#$ $" %&' ( " )*$" #" + ," reg: P 0 " #" + -" reg: P 1 " #." j |αj| 2 reg: |φ 0 '! %/P 0 " #" + ," meas1 reg: |φ 0 ! + |φ 1 !" !"#$ " #" !"#$ $"

MLLqm Proof Nets and the Correctness Criterion

Our view of MLLqm proof structures is that they are "extended quantum circuits" that allow formalization of higher-order quantum computation.

!! "#$! %&'$ "! %&'$ ! reg: 1!
As usual with proof structures, however, Def. 3.1 does not exclude proof structures that carries no computational contents-to put it technically, those which have cut nodes that cannot be eliminated. This is mainly due to vicious "feedback loops," as seen in the proof structure on the right. We exclude such feedback loops by imposing a correctness criterion that is similar to Danos and Regnier's "connected and acyclic" one [START_REF] Danos | The structure of multiplicatives[END_REF]. Then proof nets are proof structures that comply with the correctness criterion.

In the current quantum setting the challenge is to devise a graph-theoretic correctness condition for unitary gate nodes. We follow the idea in [START_REF] Dal Lago | Wave-style token machines and quantum lambda calculi[END_REF].

Definition 3.4 (Correctness graphs with quantum nodes)

Let N = (S, Q, l) be a proof structure. A correctness graph of N is an undirected graph obtained by applying the following operations to S.

-Ignore directions of all edges.

-For each `node, choose one of the two premises and disconnect the other.

-For each unitary gate node, choose an arbitrary bijective correspondence between the sets of qbit ⊥ edges and qbit edges. Remove the node and connect each correspondent pair of edges. -For each meas node, ignore its branches.

!"#$ !" #" !"#$ " !"#$ " !"#$ " !"#$ " # %&' ( " )*$" !"#$ !" !"#$ " !"#$ " #" # !"#$ " !"#$ " !" !"#$ !" " ! !"#$ !" " !"#$ !" +,"
-"

reg: |0 1 $"
Here is an example. The correctness graphs for the proof structure on the right are the four undirected graphs below. There are two choices for the ǹode and two for the unitary gate node.

!" !"#" $%&" !" !" '(" !" !"#" $%&" !" !" '(" !" !"#" $%&" !" !" '(" !" !"#" $%&" !" !" '("

Definition 3.5 (MLLqm proof nets) A correctness graph is said to satisfy the correctness criterion if it is acyclic and connected.

A proof structure N is called a proof net if each of its correctness graphs satisfies the correctness criterion and every branch in it is a proof net. Lemma 3.6 If a proof net N reduces to another proof structure N ′ (according to the rules in Def. 3.3), then N ′ is also a proof net. ⊓ ⊔

Translation of MLLqm Terms into Proof Nets

We assign a proof structure Γ ⊢ M : A to each derivable type judgment Γ ⊢ M : A. This turns out to satisfy the correctness criterion. Lem. 2.5 allows for the definition of Γ ⊢ M : A by induction on derivation.

Definition 3.7 (Translation of terms into proof nets)

For each derivable type judgment Γ ⊢ M : A, a proof structure Γ ⊢ M : A is defined inductively as in Fig. 45.

Here we let Γ ⊢ M : A = (S Γ ⊢M:A , Q Γ ⊢M:A , l Γ ⊢M:A ); and Γ denotes a sequence A 1 , A 2 , . . . , A n of types. In each case, the types A j in the context Γ of Γ ⊢ M : A appear as their dual A j ⊥ in the conclusions of S Γ ⊢M:A .

The indexing l between new nodes and quantum registers are merged in the obvious way, in the cases of Γ ⊢ M, N : A ⊗ B and Γ ⊢ M N : B .

Lemma 3.8 For any derivable type judgment Γ ⊢

M : A, the proof structure Γ ⊢ M : A is a proof net. ⊓ ⊔ x : A ⊢ x : A Γ ⊢ λx A .M : A ⊸ B ⊢ new |ϕ : qbit !"! ! "! ! ! reg: 1! reg: Q Γ, x:A ! M:B" !" ! #" " " ! " $" " " # $%&'(!&!&)("" %" # " !"#! $%&' ! reg: |φ"! Γ ⊢ M N : B ! "#! ! $%&"'# & # "# ' # ()*# ! +#!#,%&# & # $# ' %# & # $ ' %# &-# ' # &# % # '# % # reg: Q Δ ! M:A"B Q Θ ! N:A# $
where Γ = ∆, Θ and the derivation is . . . .

∆ ⊢ M : A ⊸ B . . . . Θ ⊢ N : A Γ ⊢ M N : B ⊸E Γ ⊢ M, N : A ⊗ B ! "#! ! $%&" ! '#!#(%)" ) " #" & " # ) " & " $" % " &" % " # reg: Q Δ ! M:A Q Θ ! N:B"
where Γ = ∆, Θ and the derivation is . . . .

∆ ⊢ M : A . . . . Θ ⊢ N : B Γ ⊢ M, N : A ⊗ B ⊗I Γ ⊢ λ x A , y B .M : A ⊗ B ⊸ C ⊢ U : qbit ⊗n ⊸ qbit ⊗n reg: Q Γ, x:A, y:B ! M:C" ! "#$%&'#$(&)$! ! *&+" #"
!"

' $" ) $"
!"

+ " ' $" ! ) $" ,' " % )-" &" + " $ " reg: 1! !! !! !! !! "! "! "! !! "#$% #! "#$% #! "#$% #! "#$% #! "#$% ! "#$% ! "#$% ! "#$% ! $! "#$% ! "! &! "#$% ! "! &!
Γ ⊢ if meas M then N else L : A !"#$ !" % &'# ! ()*" * " % &# ! +)*" * " * " % ,'# ! -)!"#$" !"#$' ./$" reg: Q Θ # N:A" reg: Q Θ # L:A" $" ! " $" ! " %" ! " $" ! " #0" reg: Q Δ # M:qbit"
where Γ = ∆, Θ and the derivation is . . . . Hence, regarding MLLqm proof structures as a rewriting system for quantum computation, it is sufficient to consider solely proof nets. This rewriting system exhibits the following pleasant properties (Thm. 3.9-3.10).

∆ ⊢ M : qbit . . . . Θ ⊢ N : A . . . . Θ ⊢ L : A Γ ⊢ if meas M then N else L : A

Theorem 3.9 (Termination of reduction) The reduction of MLLqm proof nets is terminating.

⊓ ⊔

Regarding reduction of proof nets as cut elimination, it is natural to expect all the cut nodes to disappear after reduction terminates. This is unfortunately not the case and we have the following restricted result (Thm. 3.10). The condition in Thm. 3.10 corresponds to the condition that a term of MLLqm is closed, i.e. has no free variable. Intuitively, it states that a proof net "executes all computation steps" if the whole input is given. ⊓ ⊔ Remark 3.11 For MLL proof nets, one of the purposes to introduce correctness criteria in [START_REF] Danos | The structure of multiplicatives[END_REF][START_REF] Girard | Linear logic[END_REF] is to characterize those proof structures which arise from some proof in sequent calculus. Therefore the converse of Lem. 3.8-so-called sequentialization-is also proved in [START_REF] Girard | Linear logic[END_REF]. It allows (re)construction of sequent calculus proofs from proof nets. However, sequentialization fails for MLLqm. Consider the following reduction; the original proof net is the translation of the term

CNOT new |0 , new |0 . !"#$! !! !! "! %&'( #! %&'( #! %&'( ! %&'( ! $ %&'( ! " %&'() %&'( ! " %&'() !*(! "! "! +,-! +,-! ./! -→ * !" !"#$ #" !"#$ #" !"#$ " !"#$ " %&$" '()" '()" *+" %&$" !"#$ " ! !"#$, %&$" %-./"
After two ⊗-`reductions we do not yet get rid of the CNOT node; it is easily seen that there is no MLLqm term that gives rise to the resulting proof net. This is a phenomenon that reflects the nonlocal character of MLLqm; and ultimately the nonlocality of quantum entanglement is to blame.

Sequentialization fails in general. Those proof nets which are sequentializable include: the net Γ ⊢ M : A (trivially); and the normal form of the net Γ ⊢ M : A for a closed term M . The latter is because Thm. 3.10 says that in that case the normal form is merely an MLL proof net with new nodes.

!"! reg: 1 ! reg: 1 ! #$!% "! &'%! ()* + ! &'%! #! ,-! #$!% "! #$!% ! #$!% ! #$!% "! #! #$!%. !"! reg: 1 ! reg: 1 ! #$!% "! &'%! &'%! #! ,-! /! #$!% "! #$!% ! &012! &'%! ()* 3 ! #$!% ! &'%! ()* 4 ! &'%! #$!% ! #$!% "! 5! #$!% "! #$!% ! !! #$!% ! ! #$!% ! $ 6! #$!% "! #$!% ! !! #$!% ! ! #$!% ! $ #$!% ! ! #$!% ! $ #$!% "! #$!% ! #$!% "! #! #$!%. #$!% ! ! #$!% ! $ 7! #$!% "! #$!% ! !! #$!% ! ! #$!% ! $ 5! #$!% "! #$!% ! !! #$!% ! ! #$!% ! $ #$!% "! #$!% ! #$!% ! reg: !(α|0 1 + β|11 ) ⊗ 1 √ 2 |0203 + 1 √ 2 |1213
Fig. 6: quantum teleportation (after some reductions irrelevant to the quantum part)

Examples and Discussion

As syntax sugar we write

x 1 , x 2 , x 3 ≡ x 1 , x 2 , x 3 and λ x A1 1 , x A2 2 , x A3 3 .M ≡ λ x A1 1 , y A2⊗A3 .((λ x A2 2 , x A3 3 .M )y)
, where y is a fresh variable. Let B :≡ λ x qbit , y qbit , z qbit . (λ v qbit , w qbit . H v, w, z )(CNOT x, y ) , C :≡ λ s qbit , t qbit , u qbit .(if meas s then Z else I) (if meas t then X else I) u , and

β 00 :≡ CNOT H new |0 , new |0
where H is the Hadamard gate, CNOT is the controlled not gate, I is the identity matrix, and Z and X are the Pauli matrices. The term β 00 denotes one of the Bell state; and the terms B and C represent the quantum circuits on the right, respectively. Quantum teleportation of one qubit α|0 + β|1 (where α, β ∈ C) is then described as a MLLqm term T :≡ λx qbit .C(B x, β 00 ) new α|0 +β|1 .

The term T is closed and has the type qbit. Its proof net translation ⊢ T : qbit , after some reductions that are irrelevant to the quantum part, is shown in Fig. 6.

It is not hard to notice the similarity between the proof net in Fig. 6 and the presentation by a quantum circuit. In general, when we translate a first-order MLLqm term the resulting proof net looks quite much like a quantum circuit. Notice that the term T is indeed first-order.

It is when higher-order functions are involved that our linear logic based approach shows its real advantage. For example, the proof net in the figure below receives a transformation E of a qubit into a qubit as an input; and feeds E with either H|ϕ or |ψ , according to the outcome of the measurement of |χ . (It is straightforward to write down an MLLqm term that gives rise to this proof net. Explicitly, the term is:

if meas new |χ then (λf qbit⊸qbit .f (H new |φ )) else (λf qbit⊸qbit .f new |ψ ).
) This is a "quantum circuit with a hole," so to speak; our current MLLqm framework can express, execute and reason about such procedures in a structural manner.

Token Machine Semantics for MLLqm Proof Nets

In this section we go on to introduce token machine semantics for MLLqm proof nets and prove its soundness, that is, the semantics is invariant under reduction of proof nets.

qbit ⊥ qbit ⊗ qbit ⊥ qbit (qbit ⊸ qbit) ⊸ qbit reg: |ϕ reg: |ψ qbit ⊥ cut new qbit reg: |χ ⊗ (qbit ⊸ qbit) ⊸ qbit new qbit ax qbit ⊥ qbit ⊗ qbit ⊥ qbit (qbit ⊸ qbit) ⊸ qbit ⊗ new qbit ax H cut qbit qbit ⊥ if
Token machines are one presentation of Girard's geometry of interaction [START_REF] Girard | Geometry of interaction 1: Interpretation of system F[END_REF]. Unlike the original presentation by C * -algebras, token machines as devised in [START_REF] Mackie | The geometry of interaction machine[END_REF] are (concrete) automata and carry a strong operational flavor. For more details see [START_REF] Pinto | Implantation Parallèle avec la Logique Linéaire (Applications des Réseaux d'Interaction et de la Géométrie de l'Interaction[END_REF].

The MLLqm token machines are different from the usual MLL ones in that it employs multiple tokens. Intuitively one token corresponds to one qubit; and they are required to synchronize when they go beyond a unitary gate node. This is one way how quantum entanglement (hence nonlocality) can be taken care of in token machine semantics. Use of multiple tokens is already in [START_REF] Dal Lago | Wave-style token machines and quantum lambda calculi[END_REF] where the style is called wave-style token machine. Multiple tokens inevitably results in nondeterminism in small-step behaviors of machines (which token moves first?). We prove confluence of small-step behaviors, and also uniqueness of big-step behaviors as its consequence. This is like in [START_REF] Dal Lago | Wave-style token machines and quantum lambda calculi[END_REF].

In the current work we go beyond [START_REF] Dal Lago | Wave-style token machines and quantum lambda calculi[END_REF] and interpret measurements too. For that purpose we rely on the ideas developed in linear logic towards accommodating additive connectives: namely (additive) slicing of proof nets, and weights in token machines. See e.g. [START_REF] Girard | Proof-nets: The parallel syntax for proof-theory[END_REF][START_REF] Laurent | A token machine for full geometry of interaction[END_REF].

Tokens

We start with usual definitions. We follow [START_REF] Laurent | A token machine for full geometry of interaction[END_REF] most closely. The presentation in [START_REF] Pinto | Implantation Parallèle avec la Logique Linéaire (Applications des Réseaux d'Interaction et de la Géométrie de l'Interaction[END_REF] is essentially the same.

Definition 4.1 (Context)

A context is defined by the following BNF: Intuitively, a token is a particle moving around the given proof net. The type occurrence A of a token indicates on which edge the token is. The context C designates which base type in A the token is concerned about. An example is A ≡ qbit ⊥ `qbit and C ≡ [ ] `qbit; token machine semantics is defined in such a way that a token's context determines which edge to take when the token hits a fork, namely a `node. The direction D of a token specifies whether it is going up or down along the edge.

C ::= [ ] | C ⊗ A | A ⊗ C | C `A | A `C ,
Finally, the natural number ζ is a feature that is not in usual MLL proof nets: it records to which qubit of a quantum register the token corresponds. When a token is deployed the initial value of ζ is 0, meaning that the token does not yet know which qubit it corresponds to. When it hits a new node new j , its index j is recorded in ζ.

The Token Machine T N

Our goal is to construct a transition system (called a token machine) T N for a given MLLqm proof net N . As an example, one state of the token machine is depicted below.

qbit ⊥ qbit ⊥ `qbit reg: 1 reg: 1 if new3 qbit ⊗ ax qbit qbit ⊥ qbit ⊗ qbit ⊥ cut X qbit ⊥ qbit qbit ⊥ `qbit I qbit ⊥ qbit qbit ⊥ `qbit qbit ⊥ cut qbit ⊥ `qbit reg: 1 reg: 1 if qbit ⊗ ax qbit ⊥ qbit ⊗ qbit ⊥ cut Z qbit ⊥ qbit qbit ⊥ `qbit I qbit ⊥ qbit qbit ⊥ `qbit cut CN OT qbit ⊥ qbit ⊥ qbit qbit cut new1 cut new2 qbit cut qbit H reg: |ϕ1 ⊗ ( 1 √ 2 |0203 + 1 √ 2 |1213 ) qbit qbit ⊥ !"#$ % !%!"#$ " &%!"#$ % !%'%(&%!&%) #
!"#$ " &%'%(&%"&%* # +%,%-.*% /%# A state of T N is roughly the data that specifies the tokens in the proof net N (how many of them, their locations, their contexts, etc.).

In the current setting of MLLqm a state carries much more data, in fact. For example it has a slicing, which is depicted by hatching the unselected branches in the above figure. It may feel strange that the selection of branches are specified even before the relevant qubits are measured: a probability-that is also carried by a state of a token machine (p = 1/2 in the above figure)-represents the likelihood of the slicing actually taken. The formal definition is as follows.

Definition 4.3 (State)

Given a proof net N = (S, Q N , l), a state of the token machine T N is a 5-tuple (Q, p, b, T pr , T ms ) where -Q is a quantum register, -p is a probability, i.e. a real number satisfying 0 ≤ p ≤ 1, -b is a slicing, -T pr is a finite set of tokens (called principal tokens), -T ms is another finite set of tokens (called measurement tokens).

A quantum register Q of a state is related to Q N (that of the proof net) but not necessarily the same-this will be clarified by definitions below of the transition relation and the initial states of T N . We go on to define the transition structure → N of T N (Def. 4.4). We note that transitions → N form a binary relation between states-without any labels or probabilities assigned to transitions. Hence T N is simply a Kripke frame. We shall refer to the transitions → N in T N also as the small-step semantics of T N .

The rules in Def. 4.4 are fairly complicated so their intuitions are stated first. The rules mainly describe how token(s) "move around the net." Almost every rule moves only one token. An exception is the U-Apply rule: it makes tokens "synchronized" and moves them at once. The if-Meas rule deletes one measurement token. The U-Apply and if-Meas rules also act on the quantum register and the probability of a state, reflecting the quantum effects of the corresponding operations. A slicing b is left untouched by transitions.

Definition 4.4 (Transition → N of the token machine T N )

The transition relation → N between states of the token machine T N is defined by the rules as in Fig. 78. Each rule except the U-Apply and if-Meas rules is divided into two rules, one for principal tokens and the other for measurement tokens.

For each rule, we informally depict the intended movement of token(s) too.

Hatching over a branch means the branch is not selected by the slicing.

Lemma 4.5 (One-step confluence)

Let N = (S, Q, l) be an MLLqm proof net. The transition relation → N of its token machine T N is one-step confluent. That is, if both s → N s 1 and s → N s 2 hold, then either s 1 = s 2 or there exists a state s ′ such that s 1 → N s ′ and s 2 → N s ′ . ⊓ ⊔

Big-Step Semantics of T N

We identify the "computational content" of a proof net N to be the big-step semantics of the token machine T N that is defined below. The big-step semantics is intuitively the correspondence between an initial state s ∈ I N and a final state s ′ ∈ F N , such that s reaches s ′ via a succession of → N . By confluence of → N (Lem. 4.5) such s ′ is shown to be unique if it exists (Prop. 4.12); hence the big-step semantics is given as a partial function I N ⇀ F N . Later in §4.4 we will show soundness, that is, the bigstep semantics is invariant under the reduction of proof nets (as defined in §3), modulo certain "quantum effects."

We start with singling out some states of T N as initial and final.

-Q = Q N ⊗ v∈V Q v b
where V is the set of all if nodes in the slice b(N ) (of any level; recall Def. 3.

2). -A token (A, C, D, ζ) belongs to T pr if and only if

• A is a conclusion edge of level 0 (recall that we denote an edge by its type occurrence); In an initial state, every principal token is at one of the conclusion edges (of level 0), waiting to go up. Measurement tokens are at query edges of any level (but only those which are in the slice b(N )). The quantum register Q keeps track not only of the level-0 register Q N but also of "internal" registers (again which are in the slice b(N )). In what follows, the transitive closure of → N is denoted by → + N .

ax ax A A ⊥ A, C, ⇑, ζ A A ⊥ A ⊥ , C ⊥ , ⇓, ζ → N ax Q, p, b, {(A, C, ⇑, ζ)} ∪ Tpr, Tms →N Q, p, b, {(A ⊥ , C ⊥ , ⇓, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(A, C, ⇑, ζ)} ∪ Tms →N Q, p, b, Tpr, {(A ⊥ , C ⊥ , ⇓, ζ)} ∪ Tms cut cut A A ⊥ A, C, ⇓, ζ A ⊥ , C ⊥ , ⇑, ζ → N cut A A ⊥ Q, p, b, {(A, C, ⇓, ζ)} ∪ Tpr, Tms →N Q, p, b, {(A ⊥ , C ⊥ , ⇑, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(A, C, ⇓, ζ)} ∪ Tms →N Q, p, b, Tpr, {(A ⊥ , C ⊥ , ⇑, ζ)} ∪ Tms ⊗-UpLeft A, C, ⇑, ζ ⊗ A B A ⊗ B A ⊗ B, C ⊗ B, ⇑, ζ ⊗ A B A ⊗ B → Q, p, b, {(A ⊗ B, C ⊗ B, ⇑, ζ)} ∪ Tpr, Tms →N Q, p, b, {(A, C, ⇑, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(A ⊗ B, C ⊗ B, ⇑, ζ)} ∪ Tms →N Q, p, b, Tpr, {(A, C, ⇑, ζ)} ∪ Tms ⊗-UpRight B, C, ⇑, ζ ⊗ A B A ⊗ B A ⊗ B, A ⊗ C, ⇑, ζ ⊗ A B A ⊗ B → Q, p, b, {(A ⊗ B, A ⊗ C, ⇑, ζ)} ∪ Tpr, Tms →N Q, p, b, {(B, C, ⇑, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(A ⊗ B, A ⊗ C, ⇑, ζ)} ∪ Tms →N Q, p, b, Tpr, {(B, C, ⇑, ζ)} ∪ Tms ⊗-DownLeft A, C, ⇓, ζ ⊗ A B A ⊗ B A ⊗ B, C ⊗ B, ⇓, ζ ⊗ A B A ⊗ B → Q, p
⊗ A B A ⊗ B A ⊗ B, A ⊗ C, ⇓, ζ ⊗ A B A ⊗ B → Q, p, b, {(B, C, ⇓, ζ)} ∪ Tpr, Tms →N Q, p, b, {(A ⊗ B, A ⊗ C, ⇓, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(B, C, ⇓, ζ)} ∪ Tms →N Q, p, b, Tpr, {(A ⊗ B, A ⊗ C, ⇓, ζ)} ∪ Tms `-UpLeft (pictures for the `rules are similar to the ⊗ rules) Q, p, b, {(A `B, C `B, ⇑, ζ)} ∪ Tpr, Tms →N Q, p, b, {(A, C, ⇑, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(A `B, C `B, ⇑, ζ)} ∪ Tms →N Q, p, b, Tpr, {(A, C, ⇑, ζ)} ∪ Tms `-UpRight Q, p, b, {(A `B, A `C, ⇑, ζ)} ∪ Tpr, Tms →N Q, p, b, {(B, C, ⇑, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(A `B, A `C, ⇑, ζ)} ∪ Tms →N Q, p, b, Tpr, {(B, C, ⇑, ζ)} ∪ Tms `-DownLeft Q, p, b, {(A, C, ⇓, ζ)} ∪ Tpr, Tms →N Q, p, b, {(A `B, C `B, ⇓, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(A, C, ⇓, ζ)} ∪ Tms →N Q, p, b, Tpr, {(A `B, C `B, ⇓, ζ)} ∪ Tms `-DownRight Q, p, b, {(B, C, ⇓, ζ)} ∪ Tpr, Tms →N Q, p, b, {(A `B, A `C, ⇓, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(B, C, ⇓, ζ)} ∪ Tms →N Q, p, b, Tpr, {(A `B, A `C, ⇓, ζ)} ∪ Tms

U-Through

U qbit ⊥ 1 qbit ⊥ n qbit ⊥ k qbit 1 qbit n qbit k qbit k , [ ], ⇑, ζ →N U qbit ⊥ 1 qbit ⊥ n qbit ⊥ k qbit 1 qbit n qbit k qbit ⊥ k , [ ], ⇓, ζ Q, p, b, {(qbit k , [ ], ⇑, ζ)} ∪ Tpr, Tms →N Q, p, b, {(qbit k ⊥ , [ ], ⇓, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(qbit k , [ ], ⇑, ζ)} ∪ Tms →N Q, p, b, Tpr, {(qbit k ⊥ , [ ], ⇓, ζ)} ∪ Tms U-Apply U qbit ⊥ 1 qbit ⊥ n qbit 1 qbit n qbit ⊥ 1 , [ ], ⇑, ζ1 qbit ⊥ n , [ ], ⇑, ζn state: Q state: U ζ1,...,ζn Q →N U qbit ⊥ 1 qbit ⊥ n qbit 1 qbit n qbit 1 , [ ], ⇓, ζ1 qbit n , [ ], ⇓, ζn Q, p, b, {(qbit ρ(1) ⊥ , [ ], ⇑, ζ ρ(1) ), . . . , (qbit ρ(m) ⊥ , [ ], ⇑, ζ ρ(m) )} ∪ Tpr, {(qbit ρ(m+1) ⊥ , [ ], ⇑, ζ ρ(m+1) ), . . . , (qbit ρ(n) ⊥ , [ ], ⇑, ζ ρ(n) )} ∪ Tms →N U ζ 1 ,...,ζn Q, p, b, {(qbit ρ(1) , [ ], ⇓, ζ ρ(1) ), . . . , (qbit ρ(m) , [ ], ⇓, ζ ρ(m) )} ∪ Tpr, {(qbit ρ(m+1) , [ ], ⇓, ζ ρ(m+1) ), . . . , (qbit ρ(n) , [ ], ⇓, ζ ρ(n) )} ∪ Tms where 0 ≤ m ≤ n and ρ is an appropriate permutation. if-Meas state: |ϕ0 +|ϕ1 state: |ϕ ′ j qbit ⊥ Γ A0 S0 S1 reg: Q0 reg: Q1 Γ0 Γ1 A1 A if qbit ⊥ Γ A0 S0 S1 reg: Q0 reg: Q1 Γ0 Γ1 A1 A if qbit, [ ], ⇑, n →N |ϕ0 + |ϕ1 , p, b, Tpr, {(qbit ⊥ , [ ], ⇑, ζ)} ∪ T ′ ms →N |ϕ ′ 0 , p j |αj

if-In

qbit ⊥ Γ A0 S0 S1 reg: Q0 reg: Q1 Γ0 Γ1 A1 A →N if qbit ⊥ Γ A0 S0 S1 reg: Q0 reg: Q1 Γ0 Γ1 A1 A if A, C, ⇑, ζ A0, C, ⇑, ζ Q, p, b, {(A, C, ⇑, ζ)} ∪ Tpr, Tms →N Q, p, b, {(Aj, C, ⇑, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(A, C, ⇑, ζ)} ∪ Tms →N Q, p, b, Tpr, {(Aj, C, ⇑, ζ)} ∪ Tms when b(v) = j where v is the if node. if-Out qbit ⊥ Γ A0 S0 S1 reg: Q0 reg: Q1 Γ0 Γ1 A1 A →N if A0, C, ⇓, ζ qbit ⊥ Γ A0 S0 S1 reg: Q0 reg: Q1 Γ0 Γ1 A1 A if A, C, ⇓, ζ Q, p, b, {(Aj , C, ⇓, ζ)} ∪ Tpr, Tms →N Q, p, b, {(A, C, ⇓, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(Aj, C, ⇓, ζ)} ∪ Tms →N Q, p, b, Tpr, {(A, C, ⇓, ζ)} ∪ Tms
Definition 4.10 (Big-step semantics) Let N be an MLLqm proof net. The big-step semantics of the token machine T N , denoted by N , is the partial function N :

I N ⇀ F N defined by N (s) := s ′ ∈ FN if s → + N s ′ ; ⊥ otherwise.
Prop. 4.12 below exhibits the legitimacy of this definition (as a partial function). It is not total but partial in general: partiality arises when the conclusion contains a qbit ⊥ . For the proof nets translated from closed MLLqm terms, it is always total (Cor. 4.16).

+ N s 1 with s 0 , s 1 ∈ F N , then s 0 = s 1 . ⊓ ⊔

Soundness of the Token Machine Semantics

Soundness of the big-step semantics-that it is invariant under the reduction of proof nets-holds only modulo certain quantum effects. The latter are formalized as follows, as suitable transformations of token machine states.

Definition 4.13 (U) Let N = (S, Q N , l) be an MLLqm proof net. Assume that there is a unitary gate node U in N for which the unitary gate reduction rule in Fig. 3 can be applied, resulting in the proof net N ′ . In this case, we define a function U : S N → S N ′ by U(Q, p, b, T pr , T ms ) := (U j1,...,jm Q, p, b, T pr , T ms ).

meas v (s) := meas v |0 (s) if b(v) = 0, meas v |1 (s) if b(v) = 1,
where s = (|ϕ , p, b, Tpr, Tms).

Intuitively, the function meas v "deletes" the if node v together with relevant entries in the slicing b. A quantum register and a probability are updated too, in an obvious manner.

Using these state transformations our main result is stated as follows.

Theorem 4.15 (Soundness) Let N → N ′ be a reduction of MLLqm proof nets. Then, 1. N = N ′ if the reduction is by the ax-cut or the ⊗-`rule.

2. N = N ′ • U if the reduction is by the unitary gate rule, where U is the corresponding unitary matrix. 3. N ≃ ( N 0 + N 1 ) • meas v if the reduction is by one of the meas rules. In this case there must be another reduction possible due to the other meas rule, and we denote the resulting two proof nets by N 0 and N 1 (N ′ is one of these). The function

N 0 + N 1 means case-distinction (recall the type I N → I N0 + I N1 of meas v ).
Here the equivalence ≃ is a natural identification of final states of T N , T N0 and

T N1 . That is, F ≃ G def. ⇐⇒ ∀x.F (x) ∼ G(x) and s ∼ s ′ def.
⇐⇒ s = s ′ disregarding slicings. Pictorially, the statements 2. and 3. say the following diagrams commute:

I N U N / / F N I N meas v N / / F N ∼ I N ′ N ′ / / F N ′ I N0 + I N1 N0 + N1 / / F N0 + F N1 . ⊓ ⊔
Thm. 4.15 together with Thm. 3.10 yield the following corollary (Cor. 4.16). This corollary implies that the computation of a closed term ends with a result. Corollary 4. [START_REF] Malherbe | Presheaf models of quantum computation: An outline[END_REF] Let N be a proof net with no qbit ⊥ in its conclusions. Then the bigstep semantics N is total. ⊓ ⊔

Example

As a concrete example we briefly look at the token machine for the proof net for quantum teleportation (Fig. 6); we shall demonstrate that the qubit α|0 1 + β|1 1 ("stored" in the node new 1 ) is transmitted correctly. The initial states of our interests are the following four:

Q, 1, b ij , (qbit, [ ], ⇑, 0) , (qbit x ⊥ , [ ], ⇓, 0), (qbit z ⊥ , [ ], ⇓, 0) ,
where Q is the quantum register (α|0

1 + β|1 1 ) ⊗ 1 √ 2 |0 2 0 3 + 1 √ 2 |1 2 1
3 and i, j ∈ {0, 1}. Each initial state (with a different slicing b ij ) corresponds to possible outcomes of the two measurements. Note that each has the probability 1.

It is straightforward to see that each of the four initial states is led to the final state α|0 + β|1 , 1/4, b ij , {(qbit, [ ], ⇓, 3)}, ∅ , with the qubit α|0 + β|1 assigned to the node new 3 . The probabilities (1/4 each) add up to 1 with the four initial states together, a fact which witnesses that the original qubit is successfully transmitted with the probability 1.

Conclusions and Future Work

We introduced the notion of MLLqm proof net. It is the first one that accommodates measurements as proof structures, and has suitable features for expressing higher-order computation thus going beyond quantum circuits.

The GoI semantics with measurements in this paper is also the first one, which was mentioned in [START_REF] Dal Lago | Wave-style token machines and quantum lambda calculi[END_REF] as one of future work. The ideas of using a form of "weakening" to capture measurements (qubits are deleted) and that states of a token machine carry probabilities are new and clean, while the overall structure of the machine follows the usual notion of slice used in linear logic.

As future work, one direction is to accommodate duplicable data, namely the bit type. Although linear logic has a standard tool-the ! modality-to handle such data, there are subtle problems coming from the no-cloning property, nonlocality, etc. Another is to accommodate recursion. We expect to be able to adapt the techniques developed in [START_REF] Mackie | The geometry of interaction machine[END_REF] and [START_REF] Hoshino | A modified GoI interpretation for a linear functional programming language and its adequacy[END_REF].

for each new node. It is clear that this does not break acyclicity and connectivity.

-For the meas rule 0 and 1, each branch is a proof net by definition. Replacing a meas node with a proof net with the same conclusion preserves correctness criterion. Thus if N is a proof net, N ′ is also a proof net. Proof. When a proof net N has n if nodes (including those inside of branches) and m unitary gate nodes of level 0, we write #N = (n, m). The proof is done by nested induction on them.

i) #N = (0, 0). Simply because of cut elimination property of MLL. The existence of new node is not relevant here: if a new node is connected to a cut node, the other edge of the cut node is necessarily connected to an ax node because of typing. ii) #N = (0, m) with 0 < m. We show that any sequence σ : N → * N ′ of reductions that has no unitary gate reduction is not maximal.

-If ax rule or ⊗-`rule can be applied to N ′ then clearly σ is not maximal.

-Suppose both ax rule and ⊗-`rule cannot be applied to N ′ . Then there are m unitary gate nodes in N ′ since any one of them is not reduced while σ. Choose one of unitary gate nodes in N ′ . If it can be reduced then σ is not maximal. Otherwise there must be some edges of type qbit ⊥ that are not connected to new nodes via cut nodes. Choose one of those edges and start a traverse along the chosen edge and go down the structure. Because of the assumption that N does not have any qbit ⊥ in its conclusions, the traverse necessarily runs into a cut node. The cut cannot be between ⊗ and `by the assumption that ⊗-`rule cannot be applied. Similarly it cannot be connected to an axiom node. Moreover it cannot be connected to new node nor if node. Hence the cut must immediately be connected to another unitary gate node, and considering types it turns out that the connection is in the form below.

!"#$ !" %" !"#$ !" !"#$ " !"#$ " &" !"#$ !" !"#$ !" !"#$ " !"#$ " '($" !"#$ " !"#$ !"
If σ is maximal, any unitary gate node cannot be reduced and thus we must be able to continue such traverse infinitely. Since a proof net is finite, that implies we will revisit a unitary gate node while the traverse. However, if such revisiting can be done then at least one correctness graph of N ′ has a cycle in it, which contradicts to the fact that N ′ is a proof net. Therefore there exists at least one unitary gate node that can be reduced and σ is not maximal. Hence by contraposition a maximal sequence of reductions must have a unitary gate reduction. Thus m will necessarily decrease. iii) #N = (n, m) with 0 < n and 0 < m. Similarly to the case ii), a maximal sequence of reductions necessarily contains a unitary gate reduction or a meas reduction. Thus either n or m will strictly decrease.

⊓ ⊔

We introduce the following notation. It will be useful in the proofs later.

Definition A.3 If a transition s → N s ′ is given by the rule r for the node v on the token t, we write s a -→ N s ′ with a := (r, v, t). We also write s

a1a2...am ------→ N s ′ if s a1 -→ N s 1 a2 -→ N s 2 a3 -→ N • • • am --→ N s ′
for some states s 1 , s 2 , . . . , s m-1 . Such a sequence a 1 a 2 . . . a m is denoted by σ, τ , etc. Observing transition rules, it can be checked that the slicings and the sets of tokens of s 1 and s 2 are the same. Thus it suffices to show that the quantum registers and the probabilities also coincide. If either a or b does not acts on quantum registers, it is clear. If both act on quantum registers, they act on disjoint qubits. Then the order of applying such two operations (unitary transformation or measurement) does not affect the resulting quantum register and probability since the tensor ⊗ in vector space is monoidal: Proof. Movement of a token can be uniquely traced back using the information carried by the token. Thus, given a token, the sequence of transitions on the token from initial state is unique. Assume there is an infinite sequence of transitions. It must have two states that have the same token because of finiteness of the net and the number of tokens. Both states have the same sequence of transitions that starts from the position in an initial state. However, there is no transition that moves a token to its initial position, therefore such sequence can occur only once. Contradiction.

(F ⊗ id)(id ⊗ E) = F ⊗ E = (id ⊗ E)(F ⊗

⊓ ⊔

A. The next lemma roughly says that, if an edge's type contains qbit, then a token with a context that designates that occurrence of qbit will eventually visit it.

→ N s 1 → N • • • → N s ′ from s to s ′ contains a state (Q, p, b, T pr , T ms ) in which a token (A, C, ⇑, ζ) is in T pr or T ms .
Proof. Assume such a token has just arrived the edge on which A occurs. Tracing back the transitions on that token yields a traverse along S. If the traverse infinitely continues, it necessarily contain an infinite loop along S. However, that situation implies there is a cycle that remains in at least one correctness graph. Hence the traverse eventually terminates and considering the type and context it ends in a conclusion or a query node, where a token start traveling in any initial state by definition. Hence indeed a token will arrive. ⊓ ⊔ Corollary A. [START_REF] Girard | Linear logic[END_REF] Let N = (S, Q, l) be an MLLqm proof net that contains a unitary gate node U that can be reduced by the unitary gate rule in Fig. 3. Assume N (s) = s ′ . Then any sequence of small transitions s → N s 1 → N • • • → N s ′ from s to s ′ contains a transition by the U-Apply rule in Fig. 8.

Proof. By Lem. A.5, for each new node that is connected to the node U and is to be reduced together, there must be a token that visit it. These tokens can only go beyond the node U by the U-Apply rule in Fig. 8; and they must do so to reach a final state s ′ .

⊓ ⊔

The next lemma says that two different tokens cannot correspond to the same qubit.

Lemma A. [START_REF] Girard | Geometry of interaction 1: Interpretation of system F[END_REF] Let N = (S, Q, l) be an MLLqm proof net. Let s 1 be an initial state of

T N and s 1 -→ N s 2 -→ N s 3 • • • -→ N s m+1 .
= ζ 2 or ζ 1 = ζ 2 = 0.
Proof. Since in an initial state all the tokens have ζ = 0, the condition ζ 1 = ζ 2 = 0 implies that the two tokens have reached the same new node. However, tracing back transitions, it is easy to see that such tokens must have come from the same conclusion with the same context. This is prohibited by the definition of initial states. ⊓ ⊔ Lemma A.8 Let N = (S, Q, l) be an MLLqm proof net with a unitary gate node U that can be reduced by the unitary gate rule in Fig. 3, resulting in the net N ′ . Consider the following transitions in the token machines T N and T

N ′ . ⇓ cut U qbit ⊥ m qbit 1 qbit m qbit ⊥ 1 new qbit qbit 1 ⇑ ⇑ ⇑ ⇓ a j b j c j d j ⇓ new qbit ⇑ x j N N ′
Here a j is a U-Through transition; b j and d j are cut transitions; and c j and x j are new transitions. Then we have

s τ a1b1c1d1a2b2c2d2•••ambmcmdmu ----------------------→ N s ′ ⇐⇒ U(s) τ x1x2•••xm -------→ N ′ s ′ ,
where s is an initial state, τ is an arbitrary sequence, and u is a U-Apply transition that involves the node U.

Proof. By induction on the number k of transitions contained in τ that affect quantum registers. Let Q be the quantum register of s. Let s 1 and s 2 be the states satisfying s τ a1b1c1d1a2b2c2d2•••ambmcmdmu ----------------------→ N s 1 and U(s)

τ x1x2•••xm
-------→ N ′ s 2 . It can easily be checked that s 1 and s 2 are the same except their quantum registers. So it suffices to show that their quantum registers coincide.

-Case k = 0. Since τ does not affect quantum registers, it is clear that the registers of s 1 and s 2 coincide with the register obtained by applying the unitary matrix U to Q. Thus s 1 = s 2 . -Case k > 0. Then τ can be written as τ 1 q 1 τ 2 q 2 • • • τ k q k where q j is a transition that acts on quantum register (i.e. by unitary gate rule or measurement rule), τ j is a sequence of transitions that does not contain such quantum transitions. Considering U can be reduced, u and q 1 act on disjoint qubits, hence U and q 1 act on disjoint qubits. Thus manipulating a quantum register first by U and second by q 1 yields the same quantum register as first by q 1 and second by U does. Hence U(s) 1. We prove the case of ax-cut rule; the case of ⊗-`rule can be proved in similar way. Let v and w be the ax node and the cut node that are under reduction, x and y be the nodes that are connected to v and w respectively. -------------------→ N s ′ also holds since σ j2 , σ j3 , σ j4 , σ j5 cannot contain any transition on t j . Repeating this argument, it can be checked that s -----------------------→ N ′ s ′ holds where x j is by new rule and a jk is on the same token as y j is. By Lem. A.8, N (s) = s ′ . ⊓ ⊔

τ1q1 ---→ N ′ s 1 ⇔ s τ1q1 ---→ N ′ s ′ 1 with U(s ′ 1 ) = s 1 . Therefore U(s) τ1q1τ2q2•••τ k q k x1x2•••xm ----------------→ N ′ s ′ ⇔ s τ1q1 ---→ N ′ s 1 and U(s 1 ) τ2q2•••τ k q k x1x2•••xm -------------→ N ′ s ′ ⇔ s τ1q1 ---→ N s 1 τ2q2•••τ k q k a1b1c1d1a2b2c2d2•••ambmcmdmu

Definition 2 . 2 (

 22 Terms of MLLqm) Terms of MLLqm are defined by: M, N, L ::

Definition 2 . 4 (

 24 Typing rules of MLLqm) Typing rules of MLLqm are shown below. A context Γ in a type judgment is a set {x 1 : A 1 , . . . , x n : A n } of variables and their types. We write its domain {x 1 , . . . , x n } as |Γ |. The juxtaposition Γ, ∆ of contexts denotes their union and we assume |Γ | ∩ |∆| = ∅.

Fig. 1 :

 1 Fig. 1: nodes of MLLqm proof structures

Fig. 3 :

 3 Fig. 3: reduction rules of MLLqm proof structures

Fig. 4 :

 4 Fig. 4: proof net translation of MLLqm terms-part I

Fig. 5 :

 5 Fig. 5: proof net translation of MLLqm terms-part II

Theorem 3 . 10 (

 310 Strong normalization) Let N = (S, Q, l) be an MLLqm proof net. If no type containing qbit ⊥ occurs in the conclusions of S, then every maximal sequence of reductions from N reaches a proof net that contains no cut nodes, no unitary gate nodes, or no if nodes.

Definition 4 . 2 (

 42 where A is a type of MLLqm. Note that every context has exactly one hole [ ]. The type obtained by substituting a type A for the hole in a context C is denoted by C[A]. A context C is called a context for A if the type A is obtained by substituting some type B for the hole [ ], i.e. A ≡ C[B]. The negation C ⊥ of a context C is defined in a natural way, e.g. (qbit ⊗ [ ]) ⊥ := qbit ⊥ `[ ]. Token) Given a proof net N = (S, Q, l), a token is a 4-tuple (A, C, D, ζ)where -A is an edge of S (we abuse notations and identify an edge and the type occurrence A assigned to it; no confusion is likely), -C is a context for A, -D is a direction, that is an element of {⇑, ⇓}, and ζ ∈ N.

Notation 4 .

 4 6 (Q v b ) Let N = (S, Q N , l) be an MLLqm proof net, b be a slicing of N , and v be an if node in S. By Q v b we denote the quantum register associated with the branch designated by b. Hence Q v b is a quantum register inside a dashed box attached to the if node v.

Definition 4 . 7 (

 47 Initial states) Let N = (S, Q N , l) be an MLLqm proof net. A state s = (Q, p, b, T pr , T ms ) of T N is said to be initial if:

  , b, {(A, C, ⇓, ζ)} ∪ Tpr, Tms →N Q, p, b, {(A ⊗ B, C ⊗ B, ⇓, ζ)} ∪ Tpr, Tms Q, p, b, Tpr, {(A, C, ⇓, ζ)} ∪ Tms →N Q, p, b, Tpr, {(A ⊗ B, C ⊗ B, ⇓, ζ)} ∪ Tms ⊗-DownRight B, C, ⇓, ζ

Fig. 7 :

 7 Fig. 7: transition rules for TN -part I

  | 2 , b, Tpr, T ′ ms when b(v) = 0 where v is the if node. |ϕ0 + |ϕ1 , p, b, Tpr, {(qbit ⊥ , [ ], ⇑, ζ)} ∪ T ′ ms →N |ϕ ′ 1 , p j |βj | 2 , b, Tpr, T ′ ms when b(v) = 1 where v is the if node.

Fig. 8 :

 8 Fig. 8: transition rules for TN -part II

Definition 4 . 8 (Definition 4 . 9 (

 4849 Final states) Let N = (S, Q N , l) be an MLLqm proof net. A state s = (Q, p, b, T pr , T ms ) of T N is said to be final if:-each principal token(A, C, D, ζ) ∈ T pr satisfies • A is a conclusion edge; • C[qbit] = A; and D = ⇓. -T ms = ∅.Therefore in a final state, all the principal tokens are back at conclusion edges, and all the measurement tokens are gone. Recall that the if-Meas transition in Def. 4.4 deletes a measurement token. Token machine) The token machine for an MLLqm proof net N is the 4-tuple T N = (S N , I N , F N , → N ) where S N is the set of states (Def. 4.3), I N and F N are the sets of initial and final states (Def. 4.7-4.8), and → N ⊆ S N × S N is the (small-step) transition relation (Def. 4.4).

Lemma 4 . 11 (Proposition 4 . 12 (

 411412 Termination of transition) Let N = (S, Q, l) be an MLLqm proof net. There is no infinite sequence of small-step transitions → N in T N .⊓ ⊔ Unique final state) Let N = (S, Q, l) be an MLLqm proof net. If s → + N s 0 and s →

Definition 4 .

 4 14 (meas)Let N = (S, Q N , l) be an MLLqm proof net. Assume that there is an if node v in N to which the meas0 and meas1 rules in Fig.3are applicable, resulting in nets N 0 and N 1 , respectively. First we define functions meas v |0 : I N → I N0 and meas v |1 : I N → I N1 , by meas v |0 |ϕ0 +|ϕ1 , p, b, Tpr, (qbit ⊥ , [ ], ⇓, ζ) ∪ Tms := |ϕ ′ 0 , p j |αj | 2 , b0, Tpr, Tms , meas v |1 |ϕ0 +|ϕ1 , p, b, Tpr, (qbit ⊥ , [ ], ⇓, ζ) ∪ Tms := |ϕ ′ 1 , p j |βj | 2 , b1, Tpr, Tms , where b j is defined by b j (u) := b(u) on every if node u in the proof net N j (j ∈ {0, 1}). Here the token (qbit ⊥ , [ ], ⇓, ζ) in the definition is on the query edge of v, and |ϕ 0 , |ϕ ′ 0 , |ϕ 1 , |ϕ ′ 1 are registers as in (1) in §3.2. Finally we define a function meas v : I N → I N0 +I N1 by (+ denotes disjoint union)

8 Proof.A. 4 9 Proof.A. 5

 8495 The fact that Γ ⊢ M : A is a proof structure can be easily checked. It is proved to be a proof net by straightforward structural induction.-The correctness graph of x : A ⊢ x : A obviously satisfies the criterion.-Connecting two conclusions of a proof structure by a `node does not yield any cycle nor disjoint components in its correctness graphs. Thus the correctness graphs of Γ ⊢ λx A .M : A ⊸ B satisfy the criterion if those of Γ, x : A ⊢ M : B satisfy the criterion. -Similarly the correctness graphs of Γ ⊢ λ x A , y B .M : A ⊗ B ⊸ C satisfy the criterion if those of Γ, x : A, y : B ⊢ M : C do so. -If all correctness graphs of ∆ ⊢ M : A ⊸ B and Θ ⊢ N : A satisfy the criterion, the construction of ∆, Θ ⊢ M N : B makes the whole structure connected and does not yield any cycle in correctness graphs. Thus the correctness graphs of ∆, Θ ⊢ M N : B satisfies the criterion. -In the same way, the correctness graphs of ∆, Θ ⊢ M, N : A ⊗ B satisfies the criterion if both ∆ ⊢ M : A and Θ ⊢ N : B do so. -The correctness graph of ⊢ new |ϕ : qbit clearly satisfies the criterion. -The correctness graphs of ⊢ U : qbit ⊗n ⊸ qbit ⊗n also satisfy the criterion. -The correctness graphs of ∆, Θ ⊢ if meas M then N else L : A obviously satisfies the criterion if those of ∆ ⊢ M : qbit do so. Both Θ ⊢ N : A and Θ ⊢ L : A are proof nets by the induction hypothesis. ⊓ ⊔ Proof of Thm. 3.Reductions of unitary gate nodes and if nodes can occur at most equal to the number of them in a net. A reduction by ⊗-`rule strictly decrease the length of types on edges, a reduction by ax-cut rule strictly decrease the number of ax node, which are both finite. Therefore reduction can occur only finitely many times. ⊓ ⊔ Proof of Thm. 3.10

Lemma A. 4

 4 Let N = (S, Q, l) be a proof net, and s ab -→ N s ′ . Assume further that b does not depend on a, that is, the token in b is not yielded by the transition a -→ N . Then we have s ba -→ N s ′ , too. Proof. Suppose s ab -→ N s 1 and s ba -→ N s 2 .

A. 6 4 )-→ N s 2 .A. 7

 6427 id) for any quantum operations F and E. Hence s 1 = s 2 . ⊓ ⊔ Proof of Lem. 4.5(as a corollary of Lem. A.Proof. Suppose s a -→ N s 1 and s b If a = b then clearly s 1 = s 2 . If a = b, then a and b are on different tokens (hence in particular b does not depend on a). In this case it is obvious that after a -→ N , a transition b -→ N is possible. Let s ′ be such that s ab -→ N s ′ ; then by Lem. A.4, we have s ba -→ N s ′ . ⊓ ⊔ Proof of Lem. 4.11

Lemma A. 5

 5 Let N = (S, Q N , l) be an MLLqm proof net and N (s) = s ′ . Let A be an edge in S of level 0 that A ≡ C[qbit]. Then any sequence of small-step transitions s

-

  ---------------------------→N s ′ (by induction hypothesis.) ⊓ ⊔ Proof. (of Thm. 4.15) Proof sketch: for N (s) = s ′ , there exists a sequence of transitions s σ -→ N s ′ . Permuting σ by Lem. A.4, we obtain σ ′ in which all the relevant transitions adjoin and s σ ′ -→ N s ′ . For such a sequence σ ′ we can easily verify that N ′ (s) = s ′ (or ( N ′ • U)(s) = s ′ or ( N ′ • meas v |0 )(s) = s ′ ) also holds. Conversely, if N ′ (s) = s ′ we can build a sequence s σ -→ N s ′ from s σ ′ -→ N ′ s ′ . Details:

  In case v has a pending edge, regard that it is connected to a dummy node with one incoming edge and no outgoing edge. Let N (s) = s ′ for s ∈ I N . Then there is a transition relation s → + N s ′ by definition of N . Since we have only one ground type qbit, either A or A ⊥ contains type qbit. Thus a token will necessarily come by Lem. A.5. Assume a token comes from x and goes to y. Then s σ1aσ2bσ3 ------→ N s ′ where a corresponds to the transition for v and b to the transition for w. By Lem. A.4, s σ1abσ2σ3 ------→ N s ′ also holds since σ 2 cannot contain any transition on t. The ax-cut reduction does not change conclusions nor quantum registers, so the initial state s of N is also an initial state of N ′ and s σ1σ2σ3 ----→ N ′ s ′ holds. Hence N ′ (s) = s ′ . The case the token comes from y and goes to x is similar. Conversely, assume N ′ (s) = s ′ for s ∈ I N ′ . If s and s ′ are related by a sequence of transition relations s σ1 -→ s ′′ σ2 -→ N s ′ where s ′′ contains a token on the edge be-tween x and y, then s σ1abσ2 ----→ N s ′ also holds, where a corresponds to the transition for v and b to the transition for w. 2. By Cor. A.6, if N (s) = s ′ then the sequence of relations can be written as s σuσ ′ ---→ N s ′ where u is the transition by the U-Apply rule for the unitary gate node on the tokens t 1 , . . . t m . Moreover, considering the fact that u can be reduced, for a token t j the sequence of relations is s σj1aj σj2bj σj3cjσj4dj σj5uσj6-------------------→N s ′ where a j , b j , c j , d j are transitions shown in the figure in Lem. A.8. By Lem. A.4, s σj1σj2σj3σj4σj5aj bj cj djuσj6

  σ1a1b1c1d1a2b2c2d2•••ambmcmdmuσ2 ------------------------→ N s ′ holds. By Lem. A.8 U(s) σ1x1x2•••xmσ2 ---------→ N ′ s ′ holds, hence ( N ′ • U)(s) = s ′ . Conversely, if ( N ′ • U)(s) = s ′ , Then by definition there is a relation s → + N ′ s ′ . By Lem. A.4, U(s) a11a12•••a1m 1 a21•••anm n x1x2•••xnσ

3 .Fig. 9 :

 39 Fig. 9: transitions x1, x2, x3meas v , it can easily be checked that s ′′ ∼ meas v (s), i.e. s ′′ and meas v (s) are the same except b. Thus meas v (s)σ -→ N ′ s ′ 0 where s ′ 0 ∼ s ′ . Conversely, if ( N ′ • meas v ) (s) σ -→ Nj s ′ j , then s x1x2x3mσ -------→ s ′where s ′ j is the same as s ′ except b.⊓ ⊔

8 Proof of Prop. 4.12 Proof

  . Newman's lemma states that, if a binary relation has no infinite sequence and is locally confluent, then it is globally confluent. Hence by Lem. 4.11 and Lem. 4.5, → N is globally confluent. It is obvious too that final states are in normal form (i.e. no outgoing → N ). These two facts yield the claim.

	⊓ ⊔
	A.9 Proof of Thm. 4.15

Acknowledgments Thanks are due to Kentaro Honda, Tristan Roussel, and Alexis Saurin for useful discussions. A.Y. and I.H. are supported by Grants-in-Aid for Young Scientists (A) No. 24680001, and by Aihara Innovative Mathematical Modeling Project, FIRST Program, JSPS/CSTP. C.F. is supported by the ANR project ANR-2010-BLAN-021301 LOGOI.

A Appendix

A.1 Proof of Lem. 2.5

Note that the rule right above a judgment Γ ⊢ M : A in its derivation is uniquely determined by the structure of M .

By the induction hypothesis |Γ, x :

for some contexts ∆ and Θ. By the induction hypothesis |∆| = FV(N ) and

Proof. By structural induction on M .

-If M ≡ x, then the derivation must be

then derivations for the judgments are in the form . . . .

By the induction hypothesis

By Lemma A.1, ∆ and Θ are uniquely determined. By the induction hypothesis

By Lemma A.1, ∆ and Θ is uniquely determined. Hence A ≡ A ′ by the induction hypothesis.

⊓ ⊔

Proof. (of Lem. 2.5) By structural induction on M .

-If M ≡ x, then the derivation must be x : A ⊢ x : A ax and thus unique.

-Similarly, if M ≡ new |ϕ or M ≡ U then the derivation is clearly unique.

-If M ≡ λx B .N and A ≡ B ⊸ C, then a derivation is in the form . . . .

By the induction hypothesis the derivation of Γ, x : Proof. What we should show is about the correctness criterion, so quantum registers are not relevant here. The statement of this lemma is well-known to hold for MLL proof nets and the existence of quantum nodes does not affect it since the ax rule and the ⊗-r ule are purely local. For the remaining rules it is also easy: