Under consideration for publication in Math Struct in Comp Science

Under consideration for publication in Math. Struct. in Comp. Science The Algebraic Lambda-Calculus L IONEL VAUX † Laboratoire de Mathématiques de l'Université de Savoie, UFR SFA, Campus Scientifique, 73376 Le Bourget-du-Lac Cedex, France E-mail: lionel. vaux@ univ-savoie. fr Received 2 May 2008; Revised 23 May 2009 We introduce an extension of the pure lambda-calculus by endowing the set of terms with a structure of vector space, or more generally of module, over 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 study a natural extension of beta-reduction in this setting: we prove it is confluent, then discuss consistency and conservativity over the ordinary lambda-calculus. We also provide normalization results for a simple type system. 1. Introduction Preliminary Definitions and Notations. Recall that a rig (or semiring with zero and unity) is the same thing as a unital ring, without the condition that every element admits an additive inverse. Let R = (R,+, 0,?, 1) be a rig: (R,+, 0) is a commutative monoid, (R,?, 1) is a monoid, ? is distributive over + and 0 is absorbing for ?.

• reduction


• linear position


• s? ?


• usual algebraic


• free variable


• confluence via usual taitmartin-löf


• algebraic ?-calculus


• can consider


• ordinary ?-term


• s? ?