Hostname: page-component-76fb5796d-dfsvx Total loading time: 0 Render date: 2024-04-25T14:51:38.159Z Has data issue: false hasContentIssue false
  • English
  • Français

The algebraic lambda calculus

Published online by Cambridge University Press:  24 August 2009

LIONEL VAUX
LIONEL VAUX*
Affiliation:
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
Get access Rights & Permissions [Opens in a new window]

Abstract

We introduce an extension of the pure lambda calculus by endowing the set of terms with the structure of a vector space, or, more generally, of a module, over a fixed set of scalars. Moreover, terms are subject to identities similar to the 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 normalisation results for a simple type system.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 19 , Issue 5 , October 2009 , pp. 1029 - 1059
Copyright
Copyright © Cambridge University Press 2009

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

Arrighi, P. and Dowek, G. (2005) A computational definition of the notion of vectorial space. Electr. Notes Theor. Comput. Sci. 117 249–261.CrossRefGoogle Scholar
Arrighi, P. and Dowek, G. (2008) Linear-algebraic lambda-calculus: higher-order, encodings, and confluence. In: Voronkov, A. (ed.) RTA. Springer-Verlag Lecture Notes in Computer Science 5117 17–31.CrossRefGoogle Scholar
Ehrhard, T. (2001) On Köthe sequence spaces and linear logic. Mathematical Structures in Computer Science 12 579–623.CrossRefGoogle Scholar
Ehrhard, T. (2005) Finiteness spaces. Mathematical Structures in Computer Science 15 (4)615–646.CrossRefGoogle Scholar
Ehrhard, T. and Regnier, L. (2003) The differential lambda-calculus. Theoretical Computer Science 309 1–41.CrossRefGoogle Scholar
Girard, J.-Y. (1987) Linear logic. Theoretical Computer Science 50 1–102.CrossRefGoogle Scholar
Girard, J.-Y. (1988) Normal functors, power series and lambda-calculus. Annals of Pure and Applied Logic 37 (2)129–177.CrossRefGoogle Scholar
Krivine, J.-L. (1990) Lambda-calcul, types et modèles, Masson, Paris.Google Scholar
Peterson, G. E. and Stickel, M. E. (1981) Complete sets of reductions for some equational theories. J. ACM 28 (2)233–264.CrossRefGoogle Scholar
Vaux, L. (2007a) The differential λμ-calculus. Theoretical Computer Science 379 (1–2)166–209.CrossRefGoogle Scholar
Vaux, L. (2007b) On linear combinations of λ-terms. In: Baader, F. (ed.) RTA. Springer-Verlag Lecture Notes in Computer Science 4533 374–388.CrossRefGoogle Scholar