科研之友
微信
新浪微博
Facebook
分享链接
摘要
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 %26quot;Scalar%26quot; 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 the Scalar type system is that it keeps track of %26apos;the amount of a type%26apos; that is present in each term. As an example of its use, we show 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.
- 出版日期2012
