一句话：提出扩展 Lambda 演算的线性代数演算 Lineal，允许任意线性组合项，给出重写规则并证明合流。
本文为向量空间与双线性函数给出一种计算式定义，并据此引入最小语言 Lineal，将高阶计算与线性代数结合。该语言扩展 Lambda 演算，允许构造任意线性组合 alpha.t + beta.u。作者用少量重写规则描述其执行方式，并依据“语言应是线性算子语言”与“应保持高阶性”两个基本要求为规则提供理据。文章进一步指出量子电路可容易编码进该演算，展示其在量子计算中的前景，并最终证明了整个演算的合流性。
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