de Mathématiques de Luminy
Lambda-calculus in an algebraic setting.
We define an extension of λ-calculus with linear combinations of terms, with coefficients taken in a fixed rig R. We extend β-reduction on these 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 R is a positive rig (i.e. a sum of scalars is zero iff all of them are zero), we show that this algebraic λ-calculus is a conservative extension of ordinary λ-calculus: two ordinary λ-terms equalized by the reduction of algebraic λ-calculus are β-equal. Last, we prove that under some reasonably minimal conditions on R, simply typed algebraic λ-terms are strongly normalizing.