On linear combinations of lambda-terms

International audienceWe define an extension of lambda-calculus with linear combinations, endowing the set of terms with a structure of R-module, where R is a fixed set of scalars. Terms are moreover subject to identities similar to usual pointwise definition of linear combinations of functions with values in a vector space. We then extend beta-reduction on those algebraic lambda-terms as follows: at + u reduces to at + u as soon as term t reduces to t and a is a non-zero scalar. We prove that reduction is confluent. Under the assumption that the set R of scalars is positive (i.e. a sum of scalars is zero iff all of them are zero), we show that this algebraic lambda-calculus is a conservative extension of ordinary lambda-calculus. On the other hand, we show that if R admits negative elements, then every term reduces to every other term. We investigate the causes of that collapse, and discuss some possible fixes