Lineal: A linear-algebraic Lambda-calculus

We provide a computational definition of the notions of vector space andbilinear functions. We use this result to introduce a minimal languagecombining higher-order computation and linear algebra. This language extendsthe Lambda-calculus with the possibility to make arbitrary linear combinationsof terms alpha.t + beta.u. We describe how to "execute" this language in termsof a few rewrite rules, and justify them through the two fundamentalrequirements that the language be a language of linear operators, and that itbe higher-order. We mention the perspectives of this work in the field ofquantum computation, whose circuits we show can be easily encoded in thecalculus. 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 : LMC