We provide a computational definition of the notions of vector space and bilinear functions. We use this result to introduce a minimal language combining higher-order computation and linear algebra. This language extends the Lambda-calculus with the possibility to make arbitrary linear combinations of terms alpha.t + beta.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.

Comment: The complementary note "On the critical pairs of a rewrite system for vector spaces" is provided in the source files. Short version :
"Linear-algebraic Lambda-calculus : higher-order and confluence", Proceedings of RTA 08, Hagenberg, July 2008. LNCS 5117, 17, (2008). Long version : LMCS

• 03B40 - Combinatory logic and lambda calculus
• 68N18 - Functional programming and lambda calculus
• 68Q42 - Grammars and rewriting systems
• 81P68 - Quantum computation