Lower bounds for scalars in a typed algebraic lambda-calculus
msra(2011)
摘要
The linear-algebraic {\lambda}-calculus is an untyped {\lambda}-calculus
extended with arbitrary linear combinations of terms. As shown by previous
works, building a type system on top of it is a delicate matter. A
straightforward extension of a classic type system, like System F, would impose
an undesirable restriction: it would only allow superpositions of terms of the
same type. Adding sums of types lifts this restriction but raises the question
of how to deal with the interaction between scalars and additions. We propose a
type system with sums of types for the linear-algebraic {\lambda}-calculus
which provides an answer to this question by allowing types to have some degree
of imprecision. The proposed type system has a subject reduction property and
is strongly normalising. Furthermore, we show that the additive fragment of the
calculus can be seen as an abstract interpretation of the full calculus.
更多查看译文
关键词
lambda calculus,linear algebra,lower bound,type system
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络