The Vectorial Lambda-Calculus

Abstract : We describe a type system for the linear-algebraic lambda-calculus. The type system accounts for the linear-algebraic aspects of this extension of lambda-calculus: it is able to statically describe the linear combinations of terms that will be obtained when reducing the programs. This gives rise to an original type theory where types, in the same way as terms, can be superposed into linear combinations. We prove that the resulting typed lambda-calculus is strongly normalising and features a weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.
Type de document :
Article dans une revue
Journal of Information and Computation, Elsevier, 2017, 254 (1), pp.105-139. 〈10.1016/j.ic.2017.04.001〉
Liste complète des métadonnées

https://hal.inria.fr/hal-00921087
Contributeur : Alejandro Díaz-Caro <>
Soumis le : jeudi 19 décembre 2013 - 16:10:48
Dernière modification le : jeudi 15 juin 2017 - 09:09:02

Identifiants

Citation

Pablo Arrighi, Alejandro Díaz-Caro, Benoît Valiron. The Vectorial Lambda-Calculus. Journal of Information and Computation, Elsevier, 2017, 254 (1), pp.105-139. 〈10.1016/j.ic.2017.04.001〉. 〈hal-00921087〉

Partager

Métriques

Consultations de la notice

340