With a view towards models of quantum computation and/or the interpretation of linear logic, we define a functional language where all functions are linear operators by construction. A small step operational semantic (and hence an interpreter/simulator) is provided for this language in the form of a term rewrite systems. In order to do so we begin by orienting the equations which axiomatize vectorial spaces and tensor products, to yield an algorithm for reducing vectors to a linear combination of base vectors. This term rewrite system, which is shown terminating and confluent, turns out to provide a "computational definition of the notion of vectorial space" and bilinear functions, as any mathematical structure validating the algorithm. We then move on to provide both matching constructs and lambda-calulus constructs. The "linear-algebraic lambda-calculus" hereby described is linear in a different (yet related) sense to that, say, of the linear lambda-calculus. These various notions of linearity are discussed, in reference to recent developments in quantum programming languages.

Joint work with Gilles Dowek.