Lower Bounds for Scalars in a Typed Algebraic λ-calculus

with Pablo Buiras and Alejandro Díaz-Caro. Submitted.PDF

Abstract

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.

BibTeX

@misc{BDCJ:2011,
Author = {Pablo Buiras and Alejandro D{\'\i}az Caro and Mauro Jaskelioff},
Howpublished = {Submitted},
Month = {1},
Title = {Lower Bounds for Scalars in a Typed Algebraic $\lambda$-calculus},
Year = {2011}}