A系统F计及标量
A System F accounting for scalars
摘要：
代数演算和线性代数演算扩展了代数演算，使其可以进行任意的线性组合。在本文中，我们提供了一个细粒度的，系统F型系统的线性代数演算。我们表明，这个“标量”型系统享有的主题还原属性和强规范化属性，我们的主要技术成果。后者产生了一个显着的简化的线性代数微积分本身，通过消除需要的一些限制，在其减少规则。但是，这个标量类型系统更重要的原始特性是，它跟踪每个术语中存在的“类型的数量”。作为一个使用的例子，我们证明了它可以保证一个项的范式是重心的，即它的标量和为1。
英文摘要：
The Algebraic lambda-calculus and the Linear-Algebraic lambda-calculus extend the lambda-calculus with the possibility of making arbitrary linear combinations of terms. In this paper we provide a fine-grained, System F-like type system for the linear-algebraic lambda-calculus. We show that this "scalar" type system enjoys both the subject-reduction property and the strong-normalisation property, our main technical results. The latter yields a significant simplification of the linear-algebraic lambda-calculus itself, by removing the need for some restrictions in its reduction rules. But the more important, original feature of this scalar type system is that it keeps track of 'the amount of a type' that is present in each term. As an example of its use, we shown that it can serve as a guarantee that the normal form of a term is barycentric, i.e that its scalars are summing to one.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
