Pablo Arrighi
email: pablo.arrighi@imag.fr

Gilles Dowek
email: gilles.dowek@inria.fr

Lineal: A linear-algebraic λ-calculus

We provide a computational definition of the notions of vector space and bilinear functions. We use this result to introduce a minimal language combining higherorder computation and linear algebra. This language extends the λ-calculus with the possibility to make arbitrary linear combinations of terms α.t + β.u. We describe how to "execute" this language in terms of a few rewrite rules, and justify them through the two fundamental requirements that the language be a language of linear operators, and that it be higher-order. We mention the perspectives of this work in the field of quantum computation, whose circuits we show can be easily encoded in the calculus. Finally, we prove the confluence of the entire calculus.

Motivations

Knuth and Bendix have described a method to transform an equational theory into a rewrite system [START_REF] Huet | A complete proof of correctness of the Knuth-Bendix completion algorithm[END_REF]. In this paper, we show that this can be achieved for the theory of vector spaces. This yields a computational definition of the notion of vector space. We then use this definition to merge at a fundamental level higher-order computation in its simplest and most general form, the untyped λ-calculus, together with linear algebra. We see this Linear-algebraic λ-calculus (also referred to as Lineal for short) as a platform for various applications, such as non-deterministic, probabilistic and quantum computation -each of these applications probably requiring their own type systems.

This journal paper integrates the contributions from three already published conference papers [START_REF] Arrighi | A computational definition of the notion of vector space[END_REF][START_REF] Arrighi | Linear-algebraic lambda-calculus[END_REF][START_REF] Arrighi | Linear-algebraic lambda-calculus: higher-order, encodings, confluence[END_REF]. There has been a number of recent works surrounding these papers, whose presentation we postpone till Section 8. The emphasis of the present introduction is on the original motivations behind this calculus; in the same way that the emphasis of the present paper is on providing an integrated, coherent, comprehensive presentation of the calculus without further add-ons.

Quantum programming languages

Over the last two decades, the discovery of several great algorithmic results [START_REF] Deutsch | Rapid solution of problems by quantum computation[END_REF][START_REF] Shor | Polynomial-Time Algorithms for Prime Factorization and Discrete Logarithms on a Quantum Computer[END_REF][START_REF] Grover | Quantum Mechanics Helps in Searching for a Needle in a Haystack[END_REF] has raised important expectations in the field of quantum computation. Somewhat surprisingly however these results have been expressed in the primitive model of quantum circuits -a situation which is akin to that of classical computation in the 1950s. Over the last few years a number of researchers have sought to develop quantum programming languages as a consequence. Without aiming to be exhaustive and in order to understand where the perspectives of this work come in, it helps to classify these proposals according to "how classical" versus "how quantum" they are [START_REF] Selinger | A lambda calculus for quantum computation with classical control[END_REF]. There are two ways a quantum mechanical system may evolve: according to a unitary transformation or under a measurement. The former is often thought of as "purely quantum": it is deterministic and will typically be used to obtain quantum superpositions of base vectors. The latter is probabilistic in the classical sense, and will typically be used to obtain some classical information about a quantum mechanical system, whilst collapsing the system to a mere base vector.

Note that these are only typical uses: it is well-known that one can simulate any unitary transformation by series of generalized measures on the one hand, and reduce all measures to a mere projection upon the canonical basis at the end of a computation on the other hand. It remains morally true nonetheless that measurement-based models of quantum computation tend to hide quantum superpositions behind a classical interface, whilst the unitary-based models of quantum computation tend to consider quantum superpositions as legitimate expressions of the language, and sometimes even seek to generalize their effects to control flow.

Therefore one may say that measurement-based models of quantum computation -whether reliant upon teleportation [START_REF] Nielsen | Universal quantum computation using only projective measurement, quantum memory, and preparation of the 0 state[END_REF], state transfer [START_REF] Perdrix | State transfer instead of teleportation in measurement-based quantum computation[END_REF] or more astonishingly graph states [START_REF] Raussendorf | The one-way quantum computer -a non-network model of quantum computation[END_REF] -lie on one extreme, as they keep the "quantumness" to a minimum.

A more balanced approach is to allow for both unitary transformations and quantum measurements. Such models can be said to formalize the existing algorithm description methods to a strong extent: they exhibit quantum registers upon which quantum circuits may be applied, together with classical registers and programming structures in order to store measurements results and control the computation [START_REF] Selinger | Towards a quantum programming language[END_REF]. For this reason they are the more practical route to quantum programming. Whilst this juxtaposition of "quantum data, classical control" has appeared ad-hoc and heterogeneous at first, functional-style approaches together with linear type systems [START_REF] Selinger | A lambda calculus for quantum computation with classical control[END_REF][START_REF] Altenkirch | An Algebra of Pure Quantum Programming[END_REF] have ended up producing elegant quantum programming languages.

Finally we may evacuate measures altogether -leaving them till the end of the computation and outside the formalism. This was the case for instance in [START_REF] Van Tonder | A Lambda Calculus for Quantum Computation[END_REF][START_REF] Van Tonder | Quantum Computation, Categorical Semantics and Linear Logic[END_REF], but here the control structure remained classical.

In our view, such a language becomes even more interesting once we have also overcome the need for any additional classical registers and programming structures, and aim to draw the full consequence of quantum mechanics: "quantum data, quantum control". After all, classical control can be viewed as a particular case of quantum control. Moreover, avoiding this distinction leads to a simpler language, exempt of the separation between classical and quantum expressions. Finally recent results suggest that quantum control may turn out to be more efficient that classical control in the presence of Black-box algorithms [START_REF] Oreshkov | Quantum correlations with no causal order[END_REF][START_REF] Chiribella | Beyond Quantum Computers[END_REF].

Quantum Turing Machines [START_REF] Bernstein | Quantum Complexity Theory[END_REF], for instance, lie on this other extreme, since the entire machine can be in a superposition of base vectors. Unfortunately they are a rather oblivious way to describe an algorithm. Functional-style control structure, on the other hand, seem to merge with quantum evolution descriptions in a unifying manner. The functional language we describe may give rise to a "purely quantum" programming language, but only once settled the question of restricting to unitary operators. This language is exempt of classical registers, classical control structure, measurements, and allows arbitrary quantum superpositions of base vectors.

A survey and comparison of these quantum programming languages can be found in [START_REF] Gay | Quantum programming languages: survey and bibliography[END_REF].

Current status of the language

In our view, the problem of formulating a language of higher-order computable operators upon infinite dimensional vector spaces was the first challenge that needed to be met, before even aiming to have a physically executable language. In the current state of affairs computability in vector spaces is dealt with matrices and compositions, and hence restricted to finite-dimensional systems -although this limitation is sometimes circumvented by introducing an extra classical control structure e.g. via the notions of uniform circuits or linear types. The language we provide achieves this goal of a minimal calculus for describing higher-order computable linear operators in a wide sense. Therefore this work may serve as a basis for studying wider notions of computability upon abstract vector spaces, whatever the interpretation of the vector space is (probabilities, number of computational paths leading to one result,. . . ).

The downside of this generality as far as the previously mentioned application to quantum computation are concerned is that our operators are not restricted to being unitary. A further step towards specializing our language to quantum computation would be to restrict to unitary operators, as required by quantum physics. There may be several ways to do so. A first lead would be to design an a posteriori static analysis that enforces unitarity -exactly like typability is not wired in pure lambda-calculus, but may be enforced a posteriori. A second one would be to require a formal unitarity proof from the programmer. With a term and a unitarity proof, we could derive a more standard representation of the operator, for instance in terms of a universal set of quantum gates [START_REF] Boykin | On universal and fault-taulerant quantum computing[END_REF]. This transformation may be seen as part of a compilation process.

In its current state, our language can be seen as a specification language for quantum programs, as it possesses several desirable features of such a language: it allows a high level description of algorithms without any commitment to a particular architecture, it allows the expression of black-box algorithms through the use of higher-order functionals, its notation remains close to both linear algebra and functional languages.

Besides quantum computing, this work may bring contributions to other fields, which we now develop.

Logics, calculi

In this article linearity is understood in the sense of linear algebra, which is not to be confused with linearity in the sense of Linear λ-calculus [1]. It may help the reader to draw attention to this distinction: Linear λ-calculus is a calculus whose types are formulae of Linear Logic [START_REF] Girard | Linear logic[END_REF]. In such a λ-calculus, one distinguishes linear resources, which may be neither duplicated nor discarded, from nonlinear ones, whose fate is not subjected to particular restrictions. The Linear-algebraic λ-calculus we describe does have some resemblances with the Linear λ-calculus, as well as some crucial, strongly motivated differences. Duplication of a term t is again treated cautiously, but in a different way: only terms expressing base vectors can be duplicated, which is compatible with linear algebra. As we shall see, terms of the form λx u are always base vectors. As a consequence, even when a term t cannot be duplicated the term λx t can. Since the term λx t is a function building the term t, it can be thought of as a description of t. (This suggests some possible connections between the abstraction λx, the ! bang operator of linear lambda-calculus and the ′ quote operator that transforms a term into a description of it as used for instance in LISP.) Again in connection with Linear Logic, Vaux has proposed an Algebraic λcalculus [START_REF] Vaux | On linear combinations of lambda-terms[END_REF] independently and simultaneously [START_REF] Arrighi | A computational definition of the notion of vector space[END_REF][START_REF] Arrighi | Linear-algebraic lambda-calculus[END_REF][START_REF] Arrighi | Linear-algebraic lambda-calculus: higher-order, encodings, confluence[END_REF] with ours, and which is similar in the sense that it exhibits linear combinations of terms, and different in both the reduction strategy and the set of scalars considered. We will say more about this in Section 8. His work is both a restriction (less operators) and a generalization (positive reals) of Ehrhard and Regnier's differential λ-calculus [START_REF] Ehrhard | The differential lambda-calculus[END_REF]. The functional style of programming is based on the λ-calculus together with a number of extensions, so as to make everyday programming more accessible. Hence, since the birth of functional programming there has been several theoretical studies of extensions of the λ-calculus in order to account for basic arithmetic (see for instance Dougherty's algebraic extension [START_REF] Dougherty | Adding Algebraic Rewriting to the Untyped Lambda Calculus[END_REF] for normalising terms of the λ-calculus). Lineal could again be viewed as just an extension of the λ-calculus in order to handle operations over vector spaces, and make everyday programming more accessible upon them. The main difference in approach is that here the λ-calculus is not seen as a control structure which sits on top of the vector space data structure, controlling which operations to apply and when. Rather, the λ-calculus terms themselves can be summed and weighted, hence they actually are the basis of the vector space. . . upon which they can also act. This intertwining of concepts is essential if seeking to represent parallel or probabilistic computation as it is the computation itself which must be endowed with a vector space structure. The ability to superpose λ-calculus terms in that sense takes us back to Boudol's parallel λ-calculus [START_REF] Boudol | Lambda-calculi for (strict) parallel functions[END_REF], and may also be viewed as taking part of a wave of probabilistic extensions of calculi, e.g. [START_REF] Bournez | Rewriting Logic and Probabilities, Rewriting Techniques and Applications[END_REF][START_REF] Herescu | Probabilistic asynchronous pi-calculus[END_REF][START_REF] Di Pierro | Probabilistic λ-calculus and quantitative program analysis[END_REF].

Confluence techniques

A standard way to describe how a program is executed is to give a small step operational semantic for it, in the form of a finite set rewrite rules which gradually transform a program into a value. The main theorem proved in this paper is the confluence of our language. What this means is that the order in which those transformations are applied does not affect the end result of the computation. Confluence results are milestones in the study of programming languages and more generally in the theory of rewriting. Our proof uses many of the theoretical tools that have been developed for confluence proofs in a variety of fields (local confluence and Newman's lemma; strong confluence and the Hindley-Rosen lemma) as well as the avatar lemma for parametric rewriting as introduced in [START_REF] Arrighi | A computational definition of the notion of vector space[END_REF]. These are fitted together in an elaborate architecture which may have its own interest whenever one seeks to merge a non-terminating conditional confluent rewrite system together with a terminating conditional confluent rewrite system.

Outline

Section 2 develops a computational definition of vector spaces and bilinear functions. This is achieved by taking the axioms of vector spaces and orienting them. Section 3 explains how to have a rewrite system for scalars that are enough to account for quantum computation. Section 4 presents the designing principles of the language, Section 5 formally describes the Linear-algebraic λ-calculus and its semantics. Section 6 shows that the language is expressive enough for classical and quantum computations. These are the more qualitative sections of the paper. We chose to postpone till Section 7 the various proofs of confluence, as they are more technical. Section 8 will be the opportunity to provide an overview of the most recent contributions surrounding this work. Section 9 provides a summary and some perspectives.

Computational vector spaces and bilinear functions

One way to prove the equality of two vectors expressed by terms such as 2.x + y + 3.x and 5.(x + y) + (-4).y is to transform these terms into linear combinations of the unknowns and check that the terms obtained this way are the same. This algorithm transforming a term expressing a vector into a linear combination of the unknowns is also useful to express the operational semantic of programming languages for quantum computing, because in such languages a program and its input value form a term expressing a vector whose value, the output, is a linear combination of constants. More generally, several algorithms used in linear algebra, such as matrix multiplication algorithms, transform a term expressing a vector with various constructs into a linear combination of constants.

The algorithm transforming a term expressing a vector into a linear combination of the unknowns is valid in all vector spaces. The goal of this Section is to show that, moreover, it completely defines the notion of vector space. This computational definition of the notion of vector space can be extended to define other algebraic notions such as bilinearity.

Algorithms and models

In this paper rewriting systems play a double role: they serve to provide an oriented version of the notion of vector space, and to provide a small step operational semantics for the introduced language. We now provide the standard definitions about them. Definition 1. (Rewriting) Let L be a first-order language. A rewrite system X on L is given by a finite set of rules of the form l -→ r. We define the relation -→ X as follows: t -→ X u if and only if there is an occurrence α in the term t, a rewrite rule l -→ r in X, and a substitution σ such that t |α = σl and u = t[σr] α , where t |α is the subterm of t at occurrence α, and t[v] α is the graft of v in t occurrence α. Definition 2. (AC-Rewriting) Let L be a first-order language. A AC-rewrite system X on L is given by binary function symbols f 1 , . . . , f n of the language and a finite set of rules of the form l -→ r. We define the relation = AC as the congruence generated by the associativity and commutativity axioms of the symbols f 1 , . . . , f n . We define the relation -→ X as follows: t -→ X u if and only if there exists a term t ′ such that t = AC t ′ , an occurrence α in t ′ , a rewrite rule l -→ r in X and a substitution σ such that t ′ |α = σl and u = AC t ′ [σr] α .

Definition 3. (Algebra) Let L be a first-order language. An L-algebra is a family formed by a set M and for each symbol f of L of arity n, a function f from M n to M . The denotation t φ of a term t for an assignment φ is defined as usual: x φ = φ(x) and f (t 1 , . . . , t n ) φ = f ( t 1 , . . . , t n ). Definition 4. (Model of a rewrite system) Let L be a first-order language and X an algorithm defined by a rewrite system on terms of the language L. An L-algebra M is a model of the algorithm X, or the algorithm X is valid in the model M, (M |= X) if for all rewrite rules l -→ r of the rewrite system and for all valuations φ, l φ = r φ .

Example 1. Consider the language L formed by two binary symbols + and × and the algorithm X defined by the distributivity rules

(x + y) × z -→ (x × z) + (y × z) x × (y + z) -→ (x × y) + (x × z)
transforming for instance, the term (a + a) × a to the term a × a + a × a. The algebra {0, 1}, min, max is a model of this algorithm.

Remark 1. This definition of the validity of an algorithm in a model is strongly related with denotational semantics, as rewriting systems could also be seen as programs, and the algebraic structure as a denotational semantics. Definition 5. (Model of an AC-rewrite system) Let L be a first-order language. Let X be a AC-rewrite system. An L-algebra M is a model of the AC-rewrite system X (M |= R) if

• for all rewrite rules l -→ r of X and for all valuations φ, l φ = r φ ,

• for all AC-symbol f of X and for all valuations φ and indices i

f (x, f (y, z)) φ = f (f (x, y), z) φ f (x, y) φ = f (y, x) φ
As a consequence if t -→ * X u then for all φ, t φ = u φ .

Vector spaces: an algorithm

Let L be a 2-sorted language with a sort K for scalars and a sort E for vectors containing two binary symbols + and × of rank K, K, K , two constants 0 and 1 of sort K, a binary symbol, also written +, of rank E, E, E , a binary symbol . of rank K, E, E and a constant 0 of sort E.

To transform a term of sort E into a linear combination of the unknowns, we want to develop sums of vectors: α.(u + v) -→ α.u + α.v, but factor sums of scalars and nested products:

α.u + β.u -→ (α + β).u, α.(β.u) -→ (α × β).u.
We also need the trivial rules u + 0 -→ u, 0.u -→ 0 and 1.u -→ u. Finally, we need three more rules for confluence α.0 -→ 0, α.u + u -→ (α + 1).u, u + u -→ (1 + 1).u. As we want to be able to apply the factorization rule to a term of the form (3.x + 4.y) + 2.x, reductions in the above rewrite system must be defined modulo the associativity and commutativity of +. This leads to the following definition. Definition 6. (The rewrite system V ) The rewrite system V is the ACrewrite system where the only AC-symbol is + and the rules are

u + 0 -→ u 0.u -→ 0 1.u -→ u α.0 -→ 0 α.(β.u) -→ (α.β).u α.u + β.u -→ (α + β).u α.u + u -→ (α + 1).u u + u -→ (1 + 1).u α.(u + v) -→ α.u + α.v
To be complete, we should also transform the axioms of the theory of fields into a rewrite system, which is known to be impossible as there is no equational description of fields as a consequence of Birkhoff's HSP theorem and the fact that the class of fields is not closed under direct product [START_REF] Birkhoff | On the Structure of Abstract Algebras[END_REF].

We could switch to the theory of modules and use the fact that the axioms of the theory of rings can be transformed into a rewrite system.

An alternative is to provide term rewrite systems for specific rings or fields such as Z, Q, Q(i, √ 2), etc. as we shall do in Section 3. Notice that these rewrite system are in general richer than that of the theory of rings. For instance in the language of the rewrite system of Q(i, √

2), we have terms expressing the numbers 1/2 or √ 2 that are not in the generic language of rings. Thus we shall introduce a general notion of "scalar rewrite system" and consider an arbitrary such system. Basically the notion of a scalar rewrite systems lists the few basic properties that scalars are usually expected to have: neutral elements, associativity of +, etc. Definition 7. (Scalar rewrite system) A scalar rewrite system is a rewrite system on a language containing at least the symbols +, ×, 0 and 1 such that:

• S is terminating and ground confluent,

• for all closed terms α, β and γ, the pair of terms Later in Subsection 7.4 we shall prove that for any such scalar rewrite system S, S ∪ V is terminating and confluent. Proposition 1. Let t be a normal term whose variables are among x 1 , ..., x n . The term t is 0 or a term of the form α 1 .x i1 + ... + α k .x i k + x i k+1 + ... + x i k+l where the indices i 1 , ..., i k+l are distinct and α 1 , ..., α k are neither 0 nor 1.

Proof. The term t is a sum u 1 + ... + u n of normal terms that are not sums (we take n = 1 if t is not a sum).

A normal term that is not a sum is either 0, a variable, or a term of the form α.v. In this case, α is neither 0 nor 1 and v is neither 0, nor a sum of two vectors nor a product of a scalar by a vector, thus it is a variable.

As the term t is normal, if n > 1 then none of the u i is 0. Hence, the term t is either 0 or a term of the form

α 1 .x i1 + ... + α k .x i k + x i k+1 + ... + x i k+l
where α 1 , ..., α k are neither 0 nor 1. As the term t is normal, the indices i 1 , ..., i k+l are distinct.

Vector spaces: a computational characterization

With respect to the notion of model, algorithms play the same role as sets of axioms: an algorithm may or may not be valid in a model, exactly like a set of axioms may or may not be valid in a model.

The notion of validity may be used to study sets of axioms, typically building a model is a way to prove that some proposition is not provable from a set of axioms. But validity can also be used in the other direction: to define algebraic structures as models of some theories. For instance, given a field K = K, +, ×, 0, 1 the class of K-vector spaces can be defined as follows.

Definition 8. (Vector space)

The algebra E, +, ., 0 is a K-vector space if and only if K = K, +, ×, 0, 1 is a field and the algebra K, +, ×, 0, 1, E, +, ., 0 is a model of the 2-sorted set of axioms

∀u∀v∀w ((u + v) + w = u + (v + w)) ∀u∀v (u + v = v + u) ∀u (u + 0 = u) ∀u ∃u ′ (u + u ′ = 0) ∀u (1.u = u) ∀α∀β∀u (α.(β.u) = (α.β).u) ∀α∀β∀u ((α + β).u = α.u + β.u) ∀α∀u∀v (α.(u + v) = α.u + α.v)
We now prove that, the class of K-vector spaces can be defined as the class of models of the rewrite system V . Proposition 2. Let K = K, +, ×, 0, 1 be a field. The algebra E, +, ., 0 is a K-vector space if and only if the algebra K, +, ×, 0, 1, E, +, ., 0 is a model of the rewrite system V .

Proof. We first check that all the rules of V and the associativity and commutativity of addition are valid in all vector spaces. All of them are trivial except α.u + u = (α + 1).u, u + u = (1 + 1).u, 0.u = 0 and α.0 = 0. The first and second are consequence of 1.u = u and α.u + β.u = (α + β).u. To prove the third let u ′ be such that u + u ′ = 0. We have 0.u = 0.u + 0

= 0.u + u + u ′ = 0.u + 1.u + u ′ = 1.u + u ′ = u + u ′ = 0. The last one is a consequence of 0.u = 0 and α.(β.u) = (α.β).u.
Conversely, we prove that all axioms of vector spaces are valid in all models of V . The validity of each of them is a consequence of the validity of a rewrite rule, except ∀u∃u ′ (u + u ′ = 0) that is a consequence of u + (-1).u = 0 itself being a consequence of α.u + β.u = (α + β).u and 0.u = 0.

Vector spaces: decidability

We now show that the rewrite system V (Definition 6) permits to prove the decidability of the word problem (i.e., whether two terms express the same vector or not) for vector spaces. Definition 9. The decomposition of t along x 1 , ..., x n is the sequence α 1 , ..., α n such that if there is a subterm of the form α.x i in t, then α i = α, if there is a subterm of the form x i in t, then α i = 1, and α i = 0 otherwise. Proposition 3. Let t and u be two terms whose variables are among x 1 , ..., x n . The following propositions are equivalent:

(i) the normal forms of t and u are identical modulo AC, (ii) the equation t = u is valid in all K-vector spaces, (iii) and the denotation of t and u in K n for the assignment φ = e 1 /x 1 , ..., e n /x n , where e 1 , ..., e n is the canonical base of K n , are identical.

Proof. Proposition (i) implies proposition (ii) and proposition (ii) implies proposition (iii). Let us prove that proposition (iii) implies proposition (i).

Let t be a normal term whose variables are among x 1 , ..., x n . Assume t φ = u φ . Let e 1 , ..., e n be the canonical base of K n and φ = e 1 /x 1 , ..., e n /x n . Call α 1 , ..., α n the coordinates of t φ in e 1 , ..., e n . Then the decompositions of the normal forms of t and u are both α 1 , ..., α n and thus they are identical modulo AC.

Summary

We usually define an algebraic structure as an algebra M, f1 , . . . , fn that validates some propositions. For instance K-vector spaces are defined as the algebras E, 0, +, . that validate the equations of Definition 8.

We can, in a more computation-oriented way, define an algebraic structure as an algebra that validates an algorithm on terms constructed upon these operations. For instance K-vector spaces are are defined as the algebras E, 0, +, . that validate the algorithm V of Definition 6.

This algorithm is a well-known algorithm in linear algebra: it is the algorithm that transforms any linear expression into a linear combination of the unknowns.

If we chose a base, as will be the case in section 5, this algorithm may be used to transforms any linear expression into a linear combination of base vectors. Still the algorithm itself is not linked to any particular base and it may even be used if the unknowns represent a linearly dependent family.

This algorithm is, at a first look, only one among the many algorithms used in linear algebra, but it completely defines the notion of vector space: a vector space is any algebra where this algorithm is valid, it is any algebra where linear expressions can be transformed this way into linear combinations of the unknowns.

Bilinearity

Another important notion about vector spaces is that of bilinear functions. For instance the tensor product, matrix multiplication, the inner product and as we shall see the application in Lineal are all bilinear operations. The method we developed for a computational characterization of vector spaces extends to this notion: Definition 10. (Bilinear function) Let E, F , and G be three vector spaces on the same field. A function ⊗ from E × F to G is said to be bilinear if

(u + v) ⊗ w = (u ⊗ w) + (v ⊗ w) (α.u) ⊗ v = α.(u ⊗ v) u ⊗ (v + w) = (u ⊗ v) + (u ⊗ w) u ⊗ (α.v) = α.(u ⊗ v)
Definition 11. (Tensor product) Let E and F be two vector spaces, the pair formed by the vector space G and the bilinear function from E × F to G is a tensor product of E and F if for all bases (e i ) i∈I of E and (e ′ j ) j∈J of F the family (e i ⊗ e ′ j ) i,j is a base of G.

The corresponding algorithm is as follows:

Definition 12. (The rewrite system V ′ ) Consider a language with four sorts: K for scalars and E, F , and G for the vectors of three vector spaces, the symbols +, ×, 0, 1 for scalars, three copies of the symbols +, . and 0 for each sort E, F , and G and a symbol ⊗ of rank E, F, G .

The system V ′ is the rewrite system formed by three copies of the rules of the system V and the rules

(u + v) ⊗ w -→ (u ⊗ w) + (v ⊗ w) (α.u) ⊗ v -→ α.(u ⊗ v) u ⊗ (v + w) -→ (u ⊗ v) + (u ⊗ w) u ⊗ (α.v) -→ α.(u ⊗ v) 0 ⊗ u -→ 0 u ⊗ 0 -→ 0
Later in Subsection 7.4 we shall prove that for any such scalar rewrite system S, S ∪ V ′ is terminating and confluent.

Propositions 1-3 generalize easily.

α 1 .(x i1 ⊗ y j1 ) + ... + α k .(x i k ⊗ y j k ) + (x i k+1 ⊗ y j k+1 ) + ... + (x i k+l ⊗ y j k+l )
where the pairs of indices i 1 , j 1 , ..., i k+l , j k+l are distinct and α 1 , ..., α k are neither 0 nor 1.

Proposition 5. Let K = K, +, ×, 0, 1 be a field. The structures E, +, ., 0 , F, +, ., 0 , G, +, ., 0 are K-vector spaces and ⊗ is a bilinear function from E × F to G if and only if K, +, ×, 0, 1, E, +, ., 0, F, +, ., 0, G, +, ., 0, ⊗ is a model of the system V ′ . Proposition 6. Let t and u be two terms whose variables of sort E are among x 1 , ..., x n , whose variables of sort F are among y 1 , ..., y p , and that have no variables of sort G and K. The following propositions are equivalent:

(i) the normal forms of t and u are identical modulo AC, (ii) the equation t = u is valid in all structures formed by three vector spaces and a bilinear function, (iii) the equation t = u is valid in all structures formed by two vector spaces and their tensor product, (iv) and the denotation of t and u in K np for the assignment φ = e 1 /x 1 , ..., e n /x n , e ′ 1 /y 1 , ..., e ′ p /y p where e 1 , ..., e n is the canonical base of K n , e ′ 1 , ..., e ′ p that of K p and ⊗ is the unique bilinear function such that e i ⊗ e ′ j = e ′′ p(i-1)+j where e ′′ 1 , ..., e ′′ np is the canonical base of K np .

The field of quantum computing

As explained in Section 2.2, fields are not easily implemented as term rewrite systems. In the previous section such problems were avoided by simply assuming the provision of some scalar rewrite system, i.e., some term rewrite system for scalars having a certain number of properties (Definition 7). However if the objective is to provide a formal operational semantics for a quantum programming language, up to the point that it provides a full description of a classical simulator for the language, then we must give such a term rewrite system explicitly. The present section briefly outlines how this can be achieved.

A rewrite system for the field

Q(i, √ 2)
In the circuit model of quantum computation the emphasis was placed on the ability to approximate any unitary transform from a finite set of gates, where approximation is defined in terms of the distance induced by the supremum norm. This line of research (cf. [53,[START_REF] Kitaev | Quantum computation, algorithms and error correction[END_REF] to cite a few) has culminated with [START_REF] Boykin | On universal and fault-taulerant quantum computing[END_REF], where the following set

CN OT =     1 0 0 0 0 1 0 0 0 0 0 1 0 0 1 0     (1)
H = 1 √ 2 1 √ 2 1 √ 2 -1 √ 2 P = 1 0 0 e iπ/4
was proven to be universal, in the sense that its closure under composition, tensor product and tracing out forms a dense set relative to the set of unitary matrices -with respect to the supremum norm. Thus, the field Q(i, √ 2) is enough for quantum computation.

To define a scalar rewrite system for this field we can proceed in three steps.

• We define a scalar rewrite system for Q,

• We use Section 2.2 to define a rewrite system for the vector space of linear combination of the form:

α.1 + β. 1 √ 2 + γ.i + δ. i √ 2 .
• We use Section 2.6 to define multiplication as a bilinear AC-operation and with the rules

1 × v -→ v 1 √ 2 × 1 √ 2 -→ (1/2).1 1 √ 2 × i -→ i √ 2 1 √ 2 × i √ 2 -→ (1/2).i i × i -→ (-1/2).1 i × i √ 2 -→ (-1/2). 1 √ 2 i √ 2 × i √ 2 -→ (-1/2).1 3.2.
Restricting to the ring D(i, 1/ √ 2) For the sake of implementation we can make further simplifications. As division does not appear when composing unitary operators, the only scalars that appear in the closure of gates (1) are those obtained by additive and multiplicative closure from the elements 1, i and 1 √ 2 , i.e., elements of the ring

D(i, 1/ √ 2)
where D is the ring of numbers that have a finite dyadic development. Thus this ring is enough for quantum computing. Notice that, as noticed above, switching to the theory of ring would not be sufficient as, in order to express the gates of quantum computing, we need terms expressing the scalars i and 1/ √ 2. An implementation of this ring, along these lines, can be found in [START_REF] Arrighi | [END_REF] that builds upon Section 3.1 and [START_REF] Cohen | An efficient representation of arithmetic for term rewriting[END_REF][START_REF] Walters | Rewrite systems for integer arithmetic[END_REF] for implementing binary numbers.

Towards a higher-order language

We introduce a language combining higher-order computation and linear algebra. The syntax of this language is minimal, in the sense that it just contains the syntax of λ-calculus and the possibility to make linear combinations of terms α.t + β.u. This language is called Linear-algebraic λ-calculus, or just Lineal.

To start with, we take as the operational semantics, the rewrite rules of vector spaces of Section 2.2, the bilinearity of application of Section 2.6, and the β-reduction rule. The goal of this section is to present the issues arising. This will result in the fine-tuned system presented in Definition 13.

Higher-order λ-calculus

In quantum computing, many algorithms fall into the category of black-box algorithms. I.e., some mysterious implementation of a function f is provided to us which we call "oracle" -and we wish to evaluate some property of f , after a limited number of queries to its oracle. For instance in the Deutsch-Josza quantum algorithm, f is a function f : {false, true} n -→ {false, true} which is either constant (i.e., ∃c∀x[f (x) = c]) or balanced (i.e., |{x such that f (x) = false}| = |{x such that f (x) = true}|), and whose corresponding oracle is a unitary transformation U f :

H n+1 2 -→ H n+1 2 such that U f : x ⊗ b → x ⊗ (b ⊕ f (x))
, where H n+1 2 stands for a tensor product of n + 1 two-dimensional vector spaces, ⊗ is the tensor product and ⊕ just the addition modulo two. The aim is to determine whether f is constant or balanced, and it turns out that this can be done in one single query to its oracle. The algorithm works by applying H ⊗ n+1 upon (false ⊗ n ⊗ true), then U f , and then H ⊗ n+1 again, where H ⊗ n+1 means applying the Hadamard gate on each of the n + 1 qubits. It is clear that a desirable feature for a linear-algebraic functional language is to be able to express algorithms as a function of an oracle. E.g. we may want to define

Dj 1 ≡ λx ((H ⊗ H) (x ((H ⊗ H) (false ⊗ true))) so that Dj 1 U f reduces to (H ⊗ H) (U f ((H ⊗ H) (false ⊗ true))
). More importantly even, one must be able to express algorithms, whether they are blackbox or not, independent of the size of their input. This is what differentiates programs from fixed-size circuits acting upon finite dimensional vector spaces, and demonstrates the ability to have control flow. The way to achieve this in functional languages involves duplicating basic components of the algorithm an appropriate number of times. E.g. we may want to define some Dj operator so that (Dj n) U f reduces to the appropriate (Dj n ) U f , where n is a natural number.

Clearly the language of uniform circuits does not offer an elegant presentation for this issue. Higher-order appears to be a desirable feature to have for black-box computing, but also for expressing recursion and for high-level programming.

Reduction strategies: copying and cloning

We seek to design a λ-calculus, i.e., have the possibility to introduce and abstract upon variables, as a mean to express functions of these variables. In doing so, we must allow functions such as λx (x ⊗ x), which duplicate their argument. This is necessary for expressiveness, for instance in order to obtain the fixed point operator or any other form of iteration/recursion. Now problems come up when functions such as λx (x ⊗ x) are applied to superpositions (i.e., sums of vectors). Linear-algebra brings a strong constraint: we know that cloning is not allowed, i.e., that the operator which maps any vector ψ onto the vector ψ ⊗ ψ is not linear. In quantum computation this impossibility is referred to as the no-cloning theorem [START_REF] Wooters | A single quantum cannot be cloned[END_REF]. Most quantum programming language proposals so far consist in some quantum registers undergoing unitary transforms and measures on the one hand, together with classical registers and programming structures ensuring control flow on the other, precisely in order to avoid such problems. But as we seek to reach beyond this duality and obtain a purely quantum programming language, we need to face it in a different manner.

This problem may be seen as a confluence problem. Faced with the term (λx (x ⊗ x)) (false + true), one could either start by substituting false + true for x and get the normal form (false + true) ⊗ (false + true), or start by using the fact that all the functions defined in our language must be linear and get ((λx (x ⊗ x)) false) + ((λx (x ⊗ x)) true) and finally the normal form (false ⊗ false) + (true ⊗ true), leading to two different results. More generally, faced with a term of the form (λx t) (u+v), one could either start by substituting u + v for x, or start by applying the right-hand-side linearity of the application, breaking the confluence of the calculus. So that operations remain linear, it is clear that we must start by developing over the + first, until we reach a base vector and then apply β-reduction. By base vector we mean a term which does not reduce to a superposition. Therefore, we define a reduction strategy where the β-reduction rule is restricted to cases where the argument is a base vector, as formalized later.

With this restriction, we say that our language allows copying but not cloning [START_REF] Arrighi | Linear-algebraic lambda-calculus[END_REF][START_REF] Altenkirch | An Algebra of Pure Quantum Programming[END_REF]. It is clear that copying has all the expressiveness required in order to express control flow, since it behaves exactly like the standard β-reduction as long as the argument passed is not in a superposition. This is the appropriate linear extension of the β-reduction, philosophically it comprehends classical computation as a (non-superposed) sub-case of linear-algebraic/quantum computation.

The same applies to erasing: the term λxλy x expresses the linear operator mapping the base vector b i ⊗ b j to b i . Again this is in contrast with other programming languages where erasing is treated in a particular fashion whether for the purpose of linearity of bound variables or the introduction of quantum measurement.

Base (in)dependence

The main conceptual difficulty when seeking to let our calculus be higherorder is to understand how it combines with this idea of copying, i.e., duplicating only base vectors. Terms of the form (λx (x x)) (λx v) raise the important question of whether the λ-term λx v must be considered to be a base vector or not:

• we need to restrict (λx t) u -→ t[u/x] to "base vectors";

• we want higher-order in the traditional sense (λx t) (λy u) -→ t[λy u/x];

• therefore abstractions must be the base vectors;

• since variables will only ever be substituted by base vectors, they also are base vectors.

It is clear that there is a notion of privileged basis arising in the calculus, but without us having to a priori choose a canonical basis (e.g. we do not introduce some arbitrary orthonormal basis {|i } all of a sudden -i.e., we have nowhere specified a basis at the first-order level). The eventual algebraic consequences of this notion of a privileged basis arising only because of the higher-order level are left as a topic for further investigations. An important intuition is that (λx v) is not the vector itself, but its classical description, i.e., the machine constructing it -hence it is acceptable to be able to copy (λx v) whereas we cannot clone v.

The calculus does exactly this distinction.

Infinities & confluence

It is possible, in our calculus, to define fixed point operators. For instance for each term b we can define the term

Y b = (λx (b + (x x)) λx (b + (x x)))
Then the term Y b reduces to b + Y b , i.e., the term reductions generate a computable series of vectors (n.b + Y b ) n whose "norm" grows towards infinity. This was expected in the presence of both fixed points and linear algebra, but the appearance of such infinities entails the appearance of indefinite forms, which we must handle with great caution. Marrying the full power of untyped λ-calculus, including fixed point operators etc., with linear-algebra therefore jeopardizes the confluence of the calculus, unless we introduce some further restrictions. Thus, exactly like in elementary calculus ∞ -∞ cannot be simplified to 0, we need to introduce a restriction to the rule allowing to factor α.t + β.t into (α+β).t to the cases where t is finite. But what do we mean by finite? Notions of norm in the usual mathematical sense seem difficult to import here. In order to avoid infinities we would like to ask that t is normalizable, but this is impossible to test in general. Hence, we restrict further the rule α.t + β.t -→ (α + β).t to the case where the term t is normal. It is quite striking to see how this restriction equates the algebraic notion of "being normalized" with the rewriting notion of "being normal". The next three examples show that this indefinite form may pop up in some other, more hidden, ways. Thus, the term t we wish to factor must also be closed, so that it does not contain any hidden infinity. This discussion motivates each of the restrictions ( * ) -( * * * * ) in the rules below. These restrictions are not just a fix: they are a way to formalize vector spaces in the presence of limits/infinities. It may come as a surprise, moreover, that we are able to tame these infinities with this small added set of restrictions, and without any need for context-sensitive conditions, as we shall prove in Section 7.

A higher-order language

We consider a first-order language, called the language of scalars, containing at least constants 0 and 1 and binary function symbols + and ×. The language of vectors is a two-sorted language, with a sort for vectors and a sort for scalars, described by the following term grammar:

t ::= x | λx t | t t | 0 | α.t | t + t
where α is a term in the language of scalars.

In this paper we consider only semi-open terms, i.e., terms containing vector variables but no scalar variables. In particular all scalar terms will be closed.

As usual we write t u 1 ... u n for ...(t u 1 ) ... u n .

Definition 13 (The system L). Our small-step semantics is defined by the relation -→ L where L is the AC-rewrite system where the only AC-symbol is + and the rules are those of S, a scalar rewrite system (see Definition 7) and the union of four groups of rules E, F , A and B:

-Group E -elementary rules

u + 0 -→ u, 0.u -→ 0, 1.u -→ u, α.0 -→ 0, α.(β.u) -→ (α × β).u, α.(u + v) -→ α.u + α.v -Group F -factorisation α.u + β.u -→ (α + β).u, ( * ) α.u + u -→ (α + 1).u, ( * ) u + u -→ (1 + 1).u, ( * )
-Group A -application

(u + v) w -→ (u w) + (v w), ( * * ) w (u + v) -→ (w u) + (w v), ( * * ) (α.u) v -→ α.(u v), ( * * * ) v (α.u) -→ α.(v u), ( * * * ) 0 u -→ 0, u 0 -→ 0, -Group B -beta reduction (λx t) b -→ t[b/x] ( * * * * )
And:

( * ) the three rules apply only if u is a closed L-normal term.

( * * ) the two rules apply only if u + v is a closed L-normal term.

( * * * ) the two rules apply only if u is a closed L-normal term.

( * * * * ) the rule applies only when b is a "base vector" term, i.e., an abstraction or a variable.

Notice that the restriction ( * ), ( * * ) and ( * * * ) are well-defined as the terms to which the restrictions apply are smaller than the left-hand side of the rule. Notice also that the restrictions are stable by substitution. Hence these conditional rules could be replaced by an infinite number of non conditional rules, i.e., by replacing the restricted variables by all the closed normal terms verifying the conditions. Finally notice how the rewrite system R = S ∪ E ∪ F ∪ A, taken without restrictions, is really just the V ′ (see Definition 12) we have seen in Section 2, i.e., an oriented version of the axioms of vector spaces. Intuitively the restricted system defines a notion of vector space with infinities. Rewrite rules with closedness conditions are not new in the theory of λ-calculus (see, for instance, [START_REF] Fernandez | Closed Reductions in the λ-calculus[END_REF]).

Normal forms. We have explained why abstractions ought to be considered as "base vectors" in our calculus. We have highlighted the presence of nonterminating terms and infinities, which make it impossible to interpret the calculus in your usual vector space structure. The following two results show that terminating closed terms on the other hand can really be viewed as superpositions of abstractions.

Proposition 7. An L-closed normal form, that is not a sum, a product by a scalar, or the null vector, is an abstraction.

Proof. By induction over term structure. Let t be a closed normal term that is not a sum, a product by a scalar, or the null vector. The term t is not a variable because it is closed, hence it is either an abstraction in which case we are done, or an application. In this case it has the form u v 1 . . . v n where u, v 1 , . . . v n are normal and closed and n is different from 0. Neither u nor v 1 is a sum, a product by a scalar, or the null vector since the term being normal we then could apply rules of group A. Thus by induction hypothesis, both terms are abstractions, thus the rule B applies and the term t is not normal.

Proposition 8 (Form of closed normal forms). A L-closed normal form is either the null vector or of the form i α i .λx t i + i λx u i where the scalars are different from 0 and 1 and the abstractions are all distinct.

Proof. If the term is not the null vector it can be written as a sum of terms that are neither 0 nor sums. We partition these terms in order to group those which are weighted by a scalar and those which are not. Hence we obtain a term of the form

α ′ i .t ′ i + u ′ i
where the terms u ′ i are neither null, nor sums, nor weighted by a scalar. Hence by Proposition 7 they are abstractions. Because the whole term is normal the terms t ′ i are themselves neither null, nor sums, nor weighted by a scalar since we could apply rules of group E. Hence Proposition 7 also applies.

Encoding classical and quantum computation

The restrictions we have placed upon our language are still more permissive than those of the call-by-value λ-calculus, hence any classical computation can be expressed in the linear-algebraic λ-calculus just as it can in the call-by-value λ-calculus.

It then suffices to express the three universal quantum gates H, Phase, Cnot [START_REF] Boykin | On universal and fault-taulerant quantum computing[END_REF] which we will do next.

Encoding booleans. We encode the booleans as the first and second projections, as usual in the classical λ-calculus: true ≡ λx λy x, false ≡ λx λy y. Again, note that these are conceived as linear functions, the fact we erase the second/first argument does not mean that the term should be interpreted as a trace out or a measurement. Here is a standard example on how to use them:

Not ≡ λy y false true .

Notice that this term expresses a unitary operator upon the vector space generated by true and false, even if some subterms express non unitary ones. Encoding unary quantum gates. For the Phase gate the naive encoding will not work, i.e., Phase ≡ λy y (e i This idea of using a dummy abstraction to restrict linearity can be generalized and made more elegant with the following syntactic sugar: For the Hadamard gate the game is just the same:

• [t] ≡ λx t.
H ≡ λy y [ √ 2 2 .(false + true)] [ √ 2 2 .(false -true)]
Encoding tensors. In quantum mechanics, vectors are put together via the bilinear symbol ⊗. But because in our calculus application is bilinear, the usual encoding of pairs does just what is needed.

⊗ ≡ λx λy λf f x y , π 1 ≡ λp(p λx λy x), π 2 ≡ λp(p λx λy y),

≡ λf λg λx ⊗ f (π 1 x) g (π 2 x) E.g. H ⊗2 ≡ H H .
From there on the infix notation for tensors will be used, i.e., t ⊗ u ≡ ⊗ t u, t u ≡ t u. Encoding the Cnot gate. This binary gate is essentially a classical gate, its encoding is standard.

Cnot ≡ λx (π 1 x) ⊗ (π 1 x) Not (π 2 x) (π 2 x)
Expressing the Deutsch-Josza algorithm parametrically.

As discusses in Section 4, an advantage of a higher-order language is that it permits to express black-box algorithms, such as the Deutsch-Josza algorithm, in a parametric way. We show now how to encode this algorithm in Lineal.

Here is the well-known simple example of the Deutsch algorithm, which is the n = 1 case of the Deutsch-Josza algorithm

Dj 1 ≡ λx H ⊗2 x H ⊗2 false ⊗ true
But we can also express control structure and use them to express the dependence of the Deutsch-Josza algorithm with respect to the size of the input. Encoding the natural number n as the Church numeral n ≡ λx λf (f n x) the term (n H λy (H y)) reduces to H ⊗ n+1 and similarly the term (n true λy (false⊗ y)) reduces to false ⊗ n ⊗ true. Thus the expression of the Deutsch-Josza algorithm term of the introduction is now straightforward:

Dj ≡ λnλx (n H λy (H y)) x (n H λy (H y)) n true λy (false ⊗ y)
.

Infinite dimensional operators. Notice that our language enables us to express operators independently of the dimension of the space they apply to, even when this dimension is infinite. For instance the identity operator is not expressed as a sum of projections whose number would depend on the dimension of the space, but as the mere lambda term λx x. In this sense our language is a language of infinite dimensional computable linear operators, in the same way that matrices are a language of computable finite dimensional linear operators.

Confluence

The main theorem of this paper is the confluence of the system L. Along the way, we will also prove the confluence of the unrestricted systems V and V ′ which we introduced for the sake of our computational definition of vector spaces. This section is quite technical. A reader who is not familiar with rewriting techniques may be happy with reading just Definition 16 and Theorem 1, and then skipping to Section 8. A reader with an interest in such techniques may on the other hand find the architecture of the proof quite useful. The rationale is as follows:

• There is only a very limited set of techniques available for proving the confluence of non-terminating rewrite systems (mainly the notions of parallel reductions and strong confluence). Hence we must distinguish the non-terminating rules, which generate the infinities (the B rule), from the others (the R rules) and show that they are confluent on their own;

• We then must show that the terminating rules and the non-terminating rules commute, so that their union is confluent. (The conditions on B, F, A are key to obtaining the commutation. Without them, both subsets are confluent, but not their union.)

• The rules of R being terminating, the critical pairs lemma applies. The critical pairs can be checked automatically for the non-conditional rules, but the conditional ones must be checked by hand. Hence we must distinguish the non-conditional rules (E rules), from the others (the F and A rules).

• In order to handle the parametricity with respect to the scalars rewrite system, we shall introduce a new technique called the avatar's lemma.

The first step is to prove the confluence of the system R = S ∪ E ∪ F ∪ A, i.e., the system L of Definition 13, minus the rule B. To prove the confluence of this system we shall prove that of the system R 0 = S 0 ∪ E ∪ F ∪ A where S 0 is a small avatar of S, namely the simplest possible scalar rewrite system. Then we use the avatar lemma to extend the result from S 0 to S, hereby obtaining the confluence of R = S ∪ E ∪ F ∪ A.

Definition 14 (The rewrite system S 0 ). The system S 0 is formed by the rules

0 + α -→ α 0 × α -→ 0 1 × α -→ α α × (β + γ) -→ (α × β) + (α × γ)
where + and × are AC-symbols.

To be able to use a critical pair lemma in an AC context, we shall use a well-known technique, detailed in the Section 7.1, and introduce addenda S 0ext , E ext and F ext to the systems S 0 , E and F , with some extra rules called extension rules, but with a more restricted form of AC-rewriting and the system

R 0ext = S 0ext ∪ E ext ∪ F ext ∪ A.
The second step towards our main goal is show that the B rule, the parallel version of the rule B defined in Definition 21, is strongly confluent on the term algebra, and commutes with R * , hence giving the confluence of L (Section 7.5).

As the system R = S ∪ E ∪ F ∪ A does not deal at all with abstractions and bound variables, we have, throughout this first part of the proof, considered λx as a unary function symbol and the bound occurrences of x as constants. This way we can safely apply known theorems about first-order rewriting.

Reminder on rule extensions and the critical pairs lemma

The term ((a + 2.a) + b) + c reduces to the term ((2 + 1).a + b) + c, as it contains a subterm a + 2.a that is AC-equivalent to an instance of the left hand side of the rule α.u + u -→ (α + 1).u. The term ((2.a + b) + a) + c does not contain such a subterm, yet it can be reduced, because it is itself AC-equivalent to the term ((2.a + a) + b) + c that contain a subterm that is an instance of the left hand side of this rule. This suggests that there is a more local way to define reduction modulo AC where the first reduction is possible but not the second.

Unfortunately, the critical pair lemma for AC-rewrite system gives the confluence of this local version of AC-reduction system and not the global one we are interested in. This problem has been solved by [START_REF] Peterson | Complete Sets of Reductions for Some Equational Theories[END_REF][START_REF] Jouannaud | Completion of a Set of Rules Modulo a Set of Equations[END_REF] that show that the globally AC reduction relation is confluent if the locally AC reduction relation of an extended rewrite system is confluent.

Definition 15 (The extension rules). Let X be a AC-rewrite system with AC symbols f 1 , . . . , f n . We define the AC-rewrite system X ext as containing the same AC symbols as X, the same rules as X, plus the rules f i (t, x) -→ f i (u, x) for each rule t -→ u of X where the head symbol of t is f i . Proposition 9 (R 0ext ). The system S 0ext is formed by the rules of S 0 and the rule

(0 + α) + χ -→ α + χ (0 × α) × χ -→ 0 × χ (1 × α) × χ -→ α × χ (α × (β + γ)) × χ -→ ((α × β) + (α × γ)) × χ
The system E ext is formed by the rules of E and the rule:

(u + 0) + x -→ u + x
The system F ext is formed by the rules of F and these three rules:

(α.u + β.u) + x -→ (α + β).u + x ( * ) (α.u + u) + x -→ (α + 1).u + x ( * ) (u + u) + x -→ (1 + 1).u + x ( * )
where ( * ) imposes the three rules apply only if u is a closed normal term. The system A ext is A.

The system R 0ext is S 0ext ∪ E ext ∪ F ext ∪ A.
As usual we write t -→ * X u if and only if t = u or t -→ X . . . -→ X u. We also write t -→ ?

X u if and only if t = u or t -→ X u t -→ X;Y u if there exist a v such that t -→ X v -→ Y u, and t -→ X↓ u if t -→ * X u and u is normal for the relation X.

Termination

Proposition 10. The systems S 0ext terminates.

Proof. Consider the following interpretation (compatible with AC)

|x| s = |0| s = |1| s = 2 |t + u| s = 1 + |t| s + |u| s |t × u| s = |t| s × |u| s
Each time a term t rewrites to a term t ′ we have |t| s > |t ′ | s . Hence, the system terminates.

Proposition 11. The systems R 0ext , R ext , S ∪ V and S ∪ V ′ terminate.

Proof. [The system E ext ∪ F ext ∪ A terminates] Consider the following interpretation (compatible with AC)

|(u v)| = (3|u| + 2)(3|v| + 2) |u + v| = 2 + |u| + |v| |α.u| = 1 + 2|u| |0| = 0
Each time a term t rewrites to a term t ′ we have |t| > |t ′ |. Hence, the system terminates.

[The system R 0ext terminates]

The system R 0ext is S 0ext ∪ E ext ∪ F ext ∪ A. It is formed of two subsystems S 0ext and E ext ∪ F ext ∪ A. By definition of the function | |, if a term t S 0ext - reduces to a term t ′ then |t| = |t ′ |. Consider a R-reduction sequence. At each E ext ∪ F ext ∪ A-reduction step,
the measure of the term strictly decreases and at each S 0ext -reduction step it remains the same. Thus there are only a finite number of E ext ∪ F ext ∪ A-reduction steps in the sequence and, as S 0ext terminates, the sequence is finite.

The same argument applies for R ext , S ∪ V and S ∪ V ′ , with respect to S instead of S 0ext .

Critical pairs Definition 16 (Confluence and local confluence).

A relation X is said to be confluent if whenever t -→ * X u and t -→ * X v, there exists a term w such that u -→ * X w and v -→ * X w. A relation X is said to be locally confluent if whenever t -→ X u and t -→ X v, there exists a term w such that u -→ * X w and v -→ * X w.

Definition 17 (Critical pair). Let l -→ r and l ′ -→ r ′ be two rewrite rules of an AC-rewrite system X, let p be an occurrence in l such that l |p is not a free variable. Let σ be an AC-unifier for l |p and l ′ , the pair σr, σ(l[p ← r ′ ]) is a critical pair of the the rewrite system X.

Proposition 12 (Peterson-Stickel Theorem). If -→ Xext terminates and for each critical pair (t, u) of X ext there exists a term w such that t -→ * Xext w u -→ * Xext w. Then the relation -→ X is confluent. Proof. See [START_REF] Peterson | Complete Sets of Reductions for Some Equational Theories[END_REF], Theorems 10.5., 9.3 and 8.9.

Proposition 13. The system S 0 ∪ E is confluent. The systems S 0 ∪ V and S 0 ∪ V ′ are confluent.

Proof. First notice that (S 0 ∪ E) ext = (S 0ext ∪ E ext ) and that this system terminates (see Proposition 11). Thus by proposition 12 all we need to do is to check that all the critical pair close. As these rules are not conditional, we have used the system CIME [START_REF]The CiME Rewrite Tool[END_REF] to check this automatically. The same applies to S 0 ∪ V ext and S 0 ∪ V ′ ext . Proposition 14. The system S 0 ∪ E ∪ F is confluent.

Proof. First notice that the system (S 0ext ∪ E ∪ F ) ext = S 0ext ∪ E ext ∪ F ext and that this system terminates (see Proposition 11). Thus by proposition 12 all we need to do is to check that all the critical pair close. If both rules used are rules of the system S 0ext ∪ E ext , then the critical pair closes by Proposition 13. There are no critical pairs between S 0ext and E ext ∪ F ext . Thus, all we need to check are the critical pairs between one rule of E ext and one of F ext or one rule of F ext and one of F ext .

To find the critical pairs, we used CIME [START_REF]The CiME Rewrite Tool[END_REF]. There are 251 critical pairs, not taking the fact that some rules are conditional and thus may not apply. Indeed, among these critical pairs 81 do not verify the conditions of the rules F ext . For instance, the pair given by CIME

α.(0 + u) + u ←-0 + α.(0 + u) + u -→ (1 + α).(0 + u)
does not verify the condition because u + 0 is never closed normal: we do not need to close this pair because our conditions forbid that it opens.

We need to check the 170 other pairs by hands. Some close easily, for instance the pair 0 + α.u ←-0.u + α.u -→ (0 + α).u closes on α.u. Some other require a short analysis of the conditions. For instance, for the pair

α.u + α.v + β.(u + v) ←-α.(u + v) + β.(u + v) -→ (α + β).(u + v)
the fact that we have been able to factor α.(u+v)+β.(u+v) into (α+β).(u+v) shows that the term u + v is closed normal, thus the terms u and v are closed normal, which permits to reduce both terms to (α + β).u + (α + β).v. All the cases are analyzed in [START_REF] Arrighi | On the critical pairs of a rewrite system for vector spaces[END_REF].

Proposition 15. The system R 0 = S 0 ∪ E ∪ F ∪ A is confluent. Proof. First notice that R 0ext = S 0ext ∪ E ext ∪ F ext ∪ A
and that this system terminates (see Proposition 11). Thus by proposition 12 all we need to do is to check that all the critical pair close. If both rules used are rules of the system S 0ext ∪ E ext ∪ F ext , then the critical pair closes by Proposition 14. It is not possible that the top-level rule is in S 0ext ∪ E ext ∪ F ext and the other in A since the rules of S 0ext ∪E ext ∪F ext do not contain any application. Thus the top-level rule must be in A and the (S 0ext ∪ E ext ∪ F ext )-reduction must be performed in a non-toplevel non-variable subterm of the left-hand-side of a rule of A. By inspection of the left-hand-sides of rules S 0ext ∪ E ext ∪ F ext the subterm must be of the form u + v, α.u or 0. But this subterm cannot be of the form u + v, because, by restriction (**), the term itself would not be A-reducible. It cannot be 0 since this term is normal. Thus it is of the form α.u. As there are five rules reducing a term of this form, there are 10 critical pairs to check. Because of the conditionality of the rewrite system we check them by hand. Proof. The system S is confluent and terminating because it is a scalar rewrite system. The system S subsumes S 0 because S is a scalar rewrite system. From Proposition 15, the system R 0 = S 0 ∪ E ∪ F ∪ A is confluent. Finally, the system E ∪ F ∪ A commutes with S * . Indeed, each rule of E ∪ F ∪ A commutes with S * as each subterm of sort scalar in the left member of a rule is either a variable or 0 or 1, which are normal forms. We conclude with Proposition 16 that R = S ∪ E ∪ F ∪ A is locally confluent. Hence as it is terminating it is confluent by Newman's lemma [START_REF] Newman | On theories with a combinatorial definition of "equivalence[END_REF].The same argument applies for S ∪ V and S ∪ V ′ .

The system L

We now want to prove that the system L is confluent. With the introduction of the rule B, we lose termination, hence we cannot use Newman's lemma [START_REF] Newman | On theories with a combinatorial definition of "equivalence[END_REF] anymore. Thus we shall use for this last part techniques coming from the proof of confluence of the λ-calculus and prove that the parallel version of the B rule is strongly confluent. In our case as we have to mix the rule B with R we shall also prove that it commutes with -→ * R .

Definition 20 (Strong confluence).

A relation X is said to be strongly confluent if whenever t -→ X u and t -→ X v, there exists a term w such that u -→ X w and v -→ X w.

Definition 21 (The relation -→ B ). The relation -→ B is the smallest reflexive congruence such that if u is a base vector, t -→ B t ′ and u -→ B u ′ then

(λx t) u -→ B t ′ [u ′ /x] Proposition 18. If v 1 -→ * R w 1 then v 1 [b/x] -→ * R w 1 [b/x],
where b is a base vector.

Proof. If the reduction of v 1 to w 1 involves an application of a conditional rule, then the condition is preserved on v 1 [v 2 /x]. Indeed, substituting some term in a closed normal term yields the same term.

Proposition 19. If v 2 -→ * R w 2 then v 1 [v 2 /x] -→ * R v 1 [w 2 /x]. Proof.
The reduction is a congruence. Proposition 20. If t = u or t -→ R u and if t -→ B v then there exists w such that u -→ B w and v -→ * R w.

Proof. By induction on the structure of t. If t = u we just take w = v. Thus we focus in the rest of the proof to the case where t -→ R u.

• If t = α.t 1 the B -reduction is just an application of the congruence. We have t ′ = α.t ′ 1 with t 1 -→ B t ′ 1 and the induction hypothesis tells us that t

1 [b/x] -→ B t ′ 1 [b ′ /x]. Hence t[b/x] = α.t 1 [b/x] -→ B α.t ′ 1 [b ′ /x] = t ′ [b ′ /x].
Proposition 23 (Strong confluence of B ). If t -→ B u and t -→ B v then there exists w such that u -→ B w and v -→ B w.

Proof. By induction on the structure of t.

• If t is a variable then u = t and v = t. We take w = t.

• If t = 0 then u = 0 and v = 0. We take w = 0.

• If t = λx t 1 then u = λx u 1 with t 1 -→ B u 1 and v = λx v 1 with t 1 -→ B v 1 .
By induction hypothesis, there exists a w 1 such that u 1 -→ B w 1 and v 1 -→ B w 1 . We take w = λx w 1 .

• If t = (t 1 t 2 ) then we consider two cases.

-If the term t 1 has the form λx t 3 and t 2 is a base vector. We consider three subcases, according to the form of the B -reductions.

Either v = (v 1 v 2 ) with t 1 -→ B v 1 , t 2 -→ B v 2 , and u = (u 1 u 2 ) with t 1 -→ B u 1 , t 2 -→ B u 2 .
By induction hypothesis, there exists terms w 1 and w 2 such that u

1 -→ B w 1 , v 1 -→ B w 1 , u 2 -→ B w 2 , v 2 -→ B w 2 . We take w = (w 1 w 2 ). Or v = v 3 [v 2 /x] with t 3 -→ B v 3 , t 2 -→ B v 2 , and u = ((λx u 3 ) u 2 ) with t 3 -→ B u 3 , t 2 -→ B u 2 .
Since t 2 is a base vector, u 2 and v 2 are also base vectors. By induction hypothesis, there exist terms w 3 and

w 2 such that u 3 -→ B w 3 , v 3 -→ B w 3 , u 2 -→ B w 2 , v 2 -→ B w 2 . We take w = w 3 [w 2 /x]. We have (λx u 3 ) u 2 -→ B w 3 [w 2 /x] by definition of B . By Proposition 22 we also have v 3 [v 2 /x] -→ B w 3 [w 2 /x]. Or v = v 3 [v 2 /x] with t 3 -→ B v 3 , t 2 -→ B v 2 , and u == u 3 [u 2 /x] with t 3 -→ B u 3 , t 2 -→ B u 2 .
Since t 2 is a base vector, u 2 and v 2 are base vectors also. By induction hypothesis, there exist terms w 3 and w 2 such that u

3 -→ B w 3 , v 3 -→ B w 3 , u 2 -→ B w 2 , v 2 -→ B w 2 . We take w = w 3 [w 2 /x]. By Proposition 22 we have both u 3 [u 2 /x] -→ B w 3 [w 2 /x] and v 3 [v 2 /x] -→ B w 3 [w 2 /x]. -Otherwise the B -reduction is just an application of the congruence, i.e., v = (v 1 v 2 ) with t 1 -→ B v 1 , t 2 -→ B v 2 , and u = (u 1 u 2 ) with t 1 -→ B u 1 , t 2 -→ B u 2 .
By induction hypothesis, there exists terms w 1 and w 2 such that u

1 -→ B w 1 , v 1 -→ B w 1 , u 2 -→ B w 2 , v 2 -→ B w 2 .
We take w = (w 1 w 2 ).

• If t is a sum then the B -reduction is just an application of the congruence. The term t is AC-equivalent to a sum t 1 + t 2 , the term u is AC-equivalent to a sum u 1 + u 2 with t 1 -→ B u 1 , t 2 -→ B u 2 , and the term v is ACequivalent to a sum v 1 + v 2 such that t 1 -→ B v 1 and t 2 -→ B v 2 . By induction hypothesis, there exist terms w 1 and w 2 such that u

1 -→ B w 1 , v 1 -→ B w 1 , u 2 -→ B w 2 , v 2 -→ B w 2 .
We take w = w 1 + w 2 .

• If finally, t = α.t 1 then the B -reduction is just an application of the congruence. We have u = α.u 1 with t 1 -→ B u 1 , and v = αv 1 with t 1 -→ B v 1 . By induction hypothesis, there exists a term w 1 such that u 1 -→ B w 1 , v 1 -→ B w 1 . We take w = α.w 1 .

Proposition 24 (Hindley-Rosen lemma). If the relations X and Y are strongly confluent and commute then the relation X ∪ Y is confluent. But our supposition on Clone, also says that (Clone (α.true + β.false)) reduces to (α.true + β.false) ⊗ (α.true + β.false). Moreover the two cannot be reconciled into a common reduct, because they are normal. Hence our supposition would break the confluence; it cannot hold. Note that λx v on the other hand can be duplicated, because it is thought as the (plans of) the classical machine for building v -in other words it stands for potential parallelism rather than actual parallelism. As expected there is no way to transform v into λx v in general; confluence ensures that the calculus handles this distinction in a consistent manner.

Current works

Algebraic λ-calculus

As we have mentioned in the introduction the idea of endowing the λ-calculus with a vector space has emerged simultaneously and independently in a different context. Indeed, the exponential-free fragment of Linear Logic is a logic of resources where the propositions themselves stand for those resources -and hence cannot be discarded nor copied. When seeking to find models of this logic, one obtains a particular family of vector spaces and differentiable functions over these. It is by trying to capture back these mathematical structures into a programming language that T. Ehrhard and L. Regnier have defined the differential λ-calculus [START_REF] Ehrhard | The differential lambda-calculus[END_REF], which has an intriguing differential operator as a built-in primitive, and some notion of module of the λ-calculus terms, over the natural numbers. More recently L. Vaux [START_REF] Vaux | On linear combinations of lambda-terms[END_REF] has focused his attention on a "differential λ-calculus without differential operator", extending the module to finitely splitting positive real numbers. He obtained a confluence result in this case, which stands even in the untyped setting. More recent works on this Algebraic λ-calculus tend to consider arbitrary scalars [START_REF] Ehrhard | A finiteness structure on resource terms[END_REF][START_REF] Tasson | Algebraic Totality, towards Completeness[END_REF]. This Algebraic λ-calculus and the Linear-algebraic λ-calculus we presented in this paper are very similar not only in names: they both merge higher-order computation, be it terminating or not, in its simplest and most general form (namely the untyped λ-calculus) together with linear algebra in its simplest and most general form also (the axioms of vector spaces). Skipping over details a closer inspection unravels that:

• the application in the Algebraic λ-calculus is left linear but not right linear;

• the abstraction in the Algebraic λ-calculus is a linear unary operator;

• the rewriting is modulo vector space axioms, and these axioms are not transformed into rewrite rules of the system.

It could be said the last two points are only minor differences; design choices in some sense. Arguably those of Lineal are advantageous because they yield a more robust confluence proof, valid for arbitrary scalars. If we lift these two differences, Lineal simulates the Algebraic λ-calculus [START_REF] Arrighi | Embedding Algebraic Lambda-calculus into Lineal[END_REF]. The first point is a more important difference, with justification right within the origins of the Algebraic λ-calculus and the Differential λ-calculus. Recently, however, it has been shown that the difference really amounts to a choice between call-by-name and call-by-value oriented strategies. The encoding of one strategy into another still works [START_REF] Díaz-Caro | Valiron Equivalence of Algebraic λcalculi[END_REF] -hence it could be said that the two calculi are essentially equivalent.

Types

Whilst terms in our calculus seem to form a vector space, the very definition of a norm is difficult in our context: deciding whether a term terminates is undecidable; but these terms produce infinities, hence convergence of a vector space norm is undecidable. Related to this precise topic, L. Vaux has studied simply typed algebraic λ-calculus, ensuring convergence of a vector space norm [START_REF] Vaux | On linear combinations of lambda-terms[END_REF]. Following his work, C. Tasson has studied some model-theoretic properties of the barycentric ( α i = 1) subset of this simply typed calculus [START_REF] Tasson | Algebraic Totality, towards Completeness[END_REF]. A recent work by T. Ehrhard proves the convergence of a Taylor series expansion of Algebraic λ-calculus terms, via a System F typing system [START_REF] Ehrhard | A finiteness structure on resource terms[END_REF].

Hence, standard type systems ensure the convergence of the vector space norm of a term. And indeed it is not so hard to define a simple extension of System F that fits Lineal -just by providing the needed rules to type additions, scalar products and the null vector in some trivial manner, as we did in [START_REF] Arrighi | Scalar System F for Linear-Algebraic λ-Calculus: Towards a Quantum Physical Logic[END_REF][START_REF] Arrighi | A System F accounting for scalars[END_REF]. As expected one obtains strong normalisation from this type system. An important byproduct of this result is that one can then remove the conditions ( * ) -( * * * ) that limit the reduction rules of Lineal (see Section 5), because their purpose was really to keep indefinite forms from reducing (such as tt, with t not normal and hence potentially infinite). In other words types make Lineal into a simpler language. Yet standard type systems are unable for instance to impose upon the language that any well-typed linear combination of terms α i .t i has α i = 1. That is unless they are provided with a handle upon these scalars. This is the purpose of the scalar type system which was recently proposed [START_REF] Arrighi | Scalar System F for Linear-Algebraic λ-Calculus: Towards a Quantum Physical Logic[END_REF][START_REF] Arrighi | A System F accounting for scalars[END_REF]. This type system which manages to keep track of "the amount of a type" by summing the amplitudes of its contributing terms, and reflects this amount within the type. As an example of its uses, it was demonstrated that this provides a type system which guarantees well-definiteness of probabilistic functions in the sense that it specializes Lineal into a probabilistic, higher-order λ-calculus. We are still looking for a type system that would impose that linear combination of terms α i .t i have |α i | 2 = 1, as suited for quantum computing.

Models

The functions expressed in our language are linear operators upon the space constituted by its terms. It is strongly inspired from the more preliminary [START_REF] Arrighi | Linear-algebraic lambda-calculus[END_REF], where terms clearly formed a vector space. However because the calculus higherorder, we get forms of infinities coming into the game. Thus, the underlying algebraic structure is not as obvious as in [START_REF] Arrighi | Linear-algebraic lambda-calculus[END_REF]. Moreover one can notice already that since the non-trivial models of the untyped λ-calculus are all uncountable, the models of (Linear-)Algebraic λ-calculus are likely to be vector spaces having an uncountable basis. These are fascinating, open questions, but whose difficulty explain why we have not provided a denotational semantics for Lineal in this paper. This issue of models of (Linear-)Algebraic λ-calculus is a challenging, active topic of current research. We know of the categorical model of simply typed Lineal with fixpoints [START_REF] Valiron | A Typed, Algebraic, Computational Lambda-Calculus[END_REF], which establishes a connection between the canon and uncanon construct of Section 6 and monads à la Moggi [START_REF] Moggi | Notions of computation and monads[END_REF]. The finiteness space model of simply typed Algebraic λ-calculus [START_REF] Ehrhard | Finiteness spaces[END_REF][START_REF] Tasson | Algebraic Totality, towards Completeness[END_REF] does not easily carry through to Lineal, which is call-by-value oriented. Recently, a syntactic finiteness space model of System F algebraic λ-calculus has been developed in [START_REF] Ehrhard | A finiteness structure on resource terms[END_REF].

Conclusion

Summary

When merging the untyped λ-calculus with linear algebra one faces two different problems. First of all simple-minded duplication of a vector is a non-linear operation (cloning) unless it is restricted to base vectors and later extended linearly (copying). Second of all we can express computable but nonetheless infinite series of vectors, hence yielding some infinities and the troublesome indefinite forms. Here again this is fixed by restricting the evaluation of these indefinite forms, this time to normal vectors. Both problems show up when looking at the confluence of the Linear-algebraic λ-calculus (Lineal). The architecture of the proof of confluence seems well-suited to any non-trivial rewrite systems having both some linear algebra and some infinities as its key ingredients. Moreover the proof of confluence entails a no-cloning result for Lineal, in accordance with the linearity of quantum physics.

Perspectives

Lineal merges higher-order computation with linear algebra in a minimalistic manner. Such a foundational approach is also taking place for instance in [START_REF] Abramsky | A categorical semantics of quantum protocols LICS[END_REF] via some categorical formulations of quantum theory exhibiting nice composition laws and normal forms, without explicit states, fixed point or the possibility to replicate gate descriptions. As for [START_REF] Abramsky | A categorical semantics of quantum protocols LICS[END_REF] although we have shown that quantum computation can be encoded in our language, Lineal remains some way apart from a model of quantum computation, because it allows evolutions which are not unitary. Establishing formal connections with this categorical approach does not seem an easy matter but is part of our objectives. These connections might arise through typing. Finding a type system which specializes Lineal into a strictly quantum programming language (enforcing the unitary constraint) is not only our next step on the list, it is actually the principal aim and motivation for this work: we wish to extend the Curry-Howard isomorphism between proofs/propositions and programs/types to a linear-algebraic, quantum setting. Having merged higher-order computation with linear-algebra in a minimalistic manner, which does not depend on any particular type systems, grants us a complete liberty to now explore different forms of this isomorphism. For instance we may expect different type systems to have different fields of application, ranging from fine-grained entanglement-analysis for quantum computation [START_REF] Perdrix | Quantum entanglement analysis based on abstract interpretation[END_REF][START_REF] Prost | Reasoning about Entanglement and Separability in Quantum Higher-Order Functions[END_REF], to opening connections with linear logic [START_REF] Díaz-Caro | From Additive Logic to Linear Logic[END_REF] or even giving rise to some novel, quantitative logics [START_REF] Arrighi | Scalar System F for Linear-Algebraic λ-Calculus: Towards a Quantum Physical Logic[END_REF].

- 0 +

 0 α and α, -0 × α and 0, -1 × α and α, -α × (β + γ) and (α × β) + (α × γ), -(α + β) + γ and α + (β + γ), -α + β and β + α, -(α × β) × γ and α × (β × γ), -α × β and β × α have the same normal forms,• 0 and 1 are normal terms.

Example 2 .

 2 If we took an unrestricted factorization rule α.t+β.t -→ (α+β).t, then the term Y b -Y b would reduce to (1 + (-1)).Y b and then 0. It would also be reduce to b + Y b -Y b and then to b, breaking the confluence.

Example 3 .

 3 Consider the term (λx ((x ) -(x ))) (λy Y b ) where is any base vector, for instance false. If the term (x ) -(x ) reduced to 0 then this term would both reduce to 0 and also to Y b -Y b , breaking confluence.

Example 4 .Example 5 .

 45 If we took an unrestricted rule (t + u) v -→ (t v) + (u v) the term (λx (x ) -λx (x )) (λy Y b ) would reduce to Y b -Y b and also to 0, breaking confluence. Thus we have to restrict the rule (t + u) v -→ (t v) + (u v) to the case where t + u is normal and closed. If we took an unrestricted rule (α.u) v -→ α.(u v) then the term (α.(x + y)) Y b would reduce both to (α.x + α.y) Y b and to α.((x + y) Y b ), breaking confluence due to the previous restriction. Thus we have to restrict the rule (α.u) v -→ α.(u v) to the case where u is normal and closed.

π 4 .

 4 true) false since by bilinearity this would give Phase false -→ * L e i π 4 .false, whereas the Phase gate is supposed to place an e i π 4 only on true. The trick is to use abstraction in order to retain the e i π 4 phase on true only (where is any base vector, for instance false). Phase ≡ λy y λx (e i π 4 .true) λx false Now, the term Phase true reduces in the following way λy y λx (e i π 4 .true) λx false true -→ L true λx (e i π 4 .true) λx false = (λx λy x) λx (e i π 4 .true) λx false -→ * L (λx (e i π 4 .true)) -→ L e i π 4 .true whereas the term Phase false reduces as follows λy y λx (e i π 4 .true) λx false false -→ L false λx (e i π 4 .true) λx false = (λx λy y) λx (e i π 4 .true) λx false -→ * L (λx false) -→ L false

Pair 1 Proposition 17 .

 117 0 v ←-(0.u) v -→ 0.(u v): this critical pair closes on 0. Pair 2 u v ←-(1.u) v -→ 1.(u v): this critical pair closes on u v. Pair 3 0 v ←-(α.0) v -→ α.(0 v): this critical pair closes on 0. Pair 4 ((α × β).u) v ←-(α.(β.u)) v -→ α.((β.u) v): the term u is closed and normal by ( * * * ). Hence, the critical pair closes on (α × β).(u v). Pair 5 (α.u+α.v) w ←-(α.(u+v)) w -→ α.((u+v) w): the term u+v is closed and normal. Hence, by Proposition 8 it is of the form i β i .a i + i b i .Therefore the top reduct reduces to ( i (α × β i ) ↓ .a i + i α.b i ) w, where ↓ denotes normalization by S 0ext . We treat only the case where the terms (l × β i ) ↓ are neither 0 nor 1, the other cases being similar. Hence, we can apply rules of groupA yielding i (α × β i ) ↓ .(a i w) + i α.(b i w).It is routine to check that the bottom reduct also reduces to this term.The five next critical pairs are the symmetrical cases, permuting the left and right-hand-sides of the application. Now, when both rules are in the group A, there are 9 critical pairs to check.Pair 11 u(w+ x) + v(w + x) ←-(u + v)(w + x) -→ (u + v)w + (u + v)x: as u + vand w + x are normal and closed, so are u, v, w and x. Hence the critical pair closes on uw + ux + vw + vx. Pair 12 u(α.w) + v(α.w) ←-(u + v)(α.w) -→ α.((u + v).w): as, by ( * * ) and ( * * * ), u+v and w are closed normal terms , so are u and v. Thus the top reduct further reduces to α.(u w)+α.(v w) and the bottom reduct further reduces to α.((u w) + (v w)) and both terms reduce to α.(u w) + α.(v w). Pair 13 0 ←-(u + v)0 -→ (u0) + (v0): this critical pair closes on 0. Pair 14 α.(u(v+w)) ←-(α.u)(v+w) -→ (α.u)v+(α.u)w: the terms u and v+w are closed normal. Thus, the top reduct further reduces to α.(uv + uw) and the bottom reduct to α.(uv) + α.(uw). Hence the critical pair closes on α.(uv) + α.(uw). Pair 15 α.(u(β.v)) ←-(α.u)(β.v) -→ β.((α.u)v): as u and v are closed normal, the first term reduces to α.(β.(uv)) and the second to β.(α.(uv)) and both terms reduce to (α × β).(uv). Pair 16 α.(u0) ←-(α.u)0 -→ 0: this critical pair closes on 0. Pair 17 0 ←-0(u + v) -→ (0u) + (0v): this critical pair closes on 0. Pair 18 0 ←-0(α.u) -→ α.(0u): this critical pair closes on 0.Pair 19 0 ←-00 -→ 0: this critical pair closes on 0. For any scalar rewrite system S the systems R = S∪E∪F ∪A, S ∪ V and S ∪ V ′ are confluent.

Theorem 1 .

 1 The system L is confluent. Proof. By Proposition 17, the relation -→ R is confluent, hence -→ * R is strongly confluent. By Proposition 23, the relation -→ B is strongly confluent. By Proposition 21, the relations -→ * R and -→ B commute. Hence, by Proposition 24 the relation -→ * R ∪ -→ B is confluent. Hence, the relation -→ L is confluent. Corollary 1 (No-cloning in the Linear-algebraic λ-calculus). There is no term Clone such that for all term v, (Clone v) -→ * L (v ⊗ v). Proof. Note that the ⊗, true and false stand for the term introduced in Section 6. Say (Clone v) -→ * L (v ⊗ v) for all v. Let v = α.true + β.false be in closed normal form. Then by the A-rules we have (Clone (α.true + β.false)) -→ * L α.(Clone true) + β.(Clone false). Next according to our supposition on Clone this further reduces to α.(true ⊗ true)+β.(false ⊗ false).

  Proposition 4. Let t be a normal term whose variables of sort E are among x 1 , ..., x n , whose variables of sort F are among y 1 , ..., y p , and that has no variables of sort G and K. If t has sort E or F , then it has the same form as in Proposition 1. If it has sort G, then it has the form

  The effect of this canon[.] is to associate to any state t a base vector [t].• {t} ≡ t where is any closed normal base vector, for instance λx x. The effect of this uncanon is to lift the canon, i.e., we have the derived rule{[t]} -→ L t.Note that {.} is a "left-inverse" of [.], but not a "right inverse", just like eval and ′ (quote) in LISP. Again these hooks do not add anymore power to the calculus, in particular they do not enable cloning. We cannot clone a given state α.t + β.u, but we can copy its classical description [α.t + β.u]. For instance the function λx [x] will never "canonize" anything else than a base vector, because of restriction ( * * * * ). The phase gate can then be written

Phase ≡ λy (y [e i π 4 .true]) [false]

Acknowledgments

The authors would like to thank Alejandro Díaz-Caro, Evelyne Contejean, Philippe Jorrand, Jean-Pierre Jouannaud, Claude Marché, Simon Perdrix, Benoît Valiron and Lionel Vaux for some enlightening discussions.

The avatar lemma

Definition 18 (Subsumption). A terminating and confluent relation S subsumes a relation S 0 if whenever t -→ S0 u, t and u have the same S-normal form.

Definition 19 (Commuting relations). Two relations X and Y are said to be commuting if whenever t -→ X u and t -→ Y v, there exists a term w such that u -→ Y w and v -→ X w.

Proposition 16 (The avatar lemma). [START_REF] Arrighi | Linear-algebraic lambda-calculus[END_REF] Let X, S and S 0 be three relations defined on a set such that:

• S is terminating and confluent;

• S subsumes S 0 ;

• S 0 ∪ X is locally confluent;

• X commutes with S * .

Then, the relation S ∪ X is locally confluent.

Proof. [X can be simulated by X; S ↓]. If t -→ X u and t -→ S ↓ v, then there exists w such that u -→ S ↓ w and v -→ X;S ↓ w. Indeed by commutation of X and S * there exists a such that u -→ S * a and v -→ X a. Normalizing a under S yields the w.

[S 0 ∪ X can be simulated by (X; S ↓) ? ].

If t -→ S0∪X u and t -→ S ↓ v, then there exists w such that u -→ S ↓ w and v -→ ? X;S ↓ w. Indeed if t -→ S0 u this is just subsumption, else the first point of this proof applies.

[S ∪ X can be simulated by (X; S ↓) ? ].

If t -→ S∪X u and t -→ S ↓ v, then there exists w such that u -→ S ↓ w and v -→ ? X;S ↓ w. Indeed if t -→ S u this is just the normalization of S, else the first point of this proof applies.

[X; S ↓ is locally confluent].

If t -→ X;S ↓ u and t -→ X;S ↓ v, then there exists w such that u -→ * X;S ↓ w and v -→ * X;S ↓ w. Indeed if t -→ X a -→ S ↓ u and t -→ X b -→ S ↓ v we know from the local confluence of S 0 ∪ X that there exists c such that a -→ * S0∪X c and b -→ * S0∪X c. Normalizing c under S yields the w. This is because by the second point of the proof u -→ *

If t -→ S∪X u and t -→ S∪X v, then there exists w such that u -→ * S∪X w and v -→ * S∪X w. Indeed call t ↓ , u ↓ , v ↓ the S normalized version of t, u, v. By the third point of our proof we have t ↓ -→ ? X;S ↓ u ↓ and t ↓ -→ ? X;S ↓ v ↓ . By the fourth point of our proof there exists w such that u ↓ -→ * X;S ↓ w and v ↓ -→ * X;S ↓ w.

If the B -reduction takes place at the toplevel, then t = (λx t 1 ) t 2 , t 2 is a base vector and there exists terms v 1 and v 2 such that t

a sum, a product by a scalar or the null vector, hence the R-reduction is just an application of the congruence thus there exists terms u 1 and u 2 such that and t 1 -→ ? R u 1 and t 2 -→ ? R u 2 . Since t 2 is a base vector, u 2 is also a base vector. By induction hypothesis, there exist terms w 1 and w 2 such that u

We have (λx u 1 ) u 2 -→ B w and by Proposition 18 and 19 we also have

If the R-reduction takes place at the toplevel, we have to distinguish several cases according to the rule used for this reduction.

• If t = t 1 + 0 and u = t 1 , then there exists a term v 1 such that t 1 -→ B v 1 and v = v 1 + 0. We take w = v 1 .

• If t = 0.t 1 and u = 0, then there exists a term v 1 such that t 1 -→ B v 1 and v = 0.v 1 . We take w = 0.

We take w = v 1 .

• If t = α.0 and u = 0, then v = t. We take w = 0.

) and u = (α × β).t 1 , then there exists a term v 1 such that t 1 -→ B v 1 and v = α.(β.v 1 ). We take w = (α × β).v 1 .

• If t = α.(t 1 + t 2 ) and u = α.t 1 + α.t 2 , then there exist terms v 1 and

. We take w = α.v 1 + α.v 2 .

• If t = α.t 1 + β.t 1 and u = (α + β).t 1 , then by ( * ) t 1 is L-normal, thus v = t. We take w = u.

The cases of the two other factorisation rules are similar.

• If t = (t 1 + t 2 ) t 3 and u = t 1 t 3 + t 2 t 3 , then by ( * * ) the term t 1 + t 2 is Lnormal. There exists a term v 3 such that t 3 -→ B v 3 and v = (t 1 +t 2 ) v 3 .

We take w = t 1 v 3 + t 2 v 3 .

• If t = 0 t 2 and u = 0, then there exists a term v 2 such that t 2 -→ B v 2 and v = 0 v 2 . We take w = 0.

The three other cases where a rule of group A is applied are symmetric.

Finally if both reductions are just applications of the congruence we apply the induction hypothesis to the subterms.

Proposition 21 (-→ * R commutes with -→ B ). If t -→ * R u and t -→ B v then there exists w such that u -→ B w and v -→ * R w.

Proof. By induction on the length of the -→ * R derivation. If t = u then we take w = v. Otherwise there exists a term t 1 such that t -→ R t 1 -→ * R u with a shorter reduction from t 1 to u. Using Proposition 20, there exists a term w 1 such that t 1 -→ B w 1 and v -→ * R w 1 . By induction hypothesis, there exists a term w such that u -→ B w and w 1 -→ * R w. We have u -→ B w and v -→ * R w.

Proposition 22 (Substitution for B ).

Here b denotes a base vector.

Proof. By induction on the structure of t.

• If t = λy t 1 the B -reduction is just an application of the congruence. We have t ′ = λy .t ′ 1 with t 1 -→ B t ′ 1 and the induction hypothesis tells us that

• If t = (t 1 t 2 ) then we consider two cases.

-We have t 1 = λy t 3 , t 2 a base state, and t ′ = t ′ 3 [t ′ 2 /x], i.e., a Breduction occurs at top-level. By induction hypothesis we know that t

• If t is a sum the B -reduction is just an application of the congruence.

Therefore t is AC-equivalent to t 1 + t 2 and t ′ is AC-equivalent to t

Then by induction hypothesis we know that t