Lineal：一个线性代数Lambda演算
Lineal: A linear-algebraic Lambda-calculus
摘要：
我们提供了向量空间和双线性函数的概念的计算定义。我们使用这个结果来介绍一个最小的语言相结合的高阶计算和线性代数。这种语言扩展了λ演算，使之有可能进行α t + β 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
