Skip to Main content Skip to Navigation

The vectorial λ-calculus

Abstract : We describe a type system for the linear-algebraic λ-calculus. The type system accounts for the linear-algebraic aspects of this extension of λ-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 λ-calculus is strongly normalising and features weak subject reduction. Finally, we show how to naturally encode matrices and vectors in this typed calculus.
Document type :
Journal articles
Complete list of metadatas

Cited literature [43 references]  Display  Hide  Download

https://hal.archives-ouvertes.fr/hal-01785464
Contributor : Kévin Perrot <>
Submitted on : Monday, May 7, 2018 - 3:40:55 PM
Last modification on : Thursday, January 23, 2020 - 6:22:10 PM
Document(s) archivé(s) le : Tuesday, September 25, 2018 - 12:42:32 PM

File

1308.1138.pdf
Files produced by the author(s)

Identifiers

Citation

Pablo Arrighi, Alejandro Díaz-Caro, Benoît Valiron. The vectorial λ-calculus. Information and Computation, Elsevier, 2017, 254 (1), pp.105--139. ⟨10.1016/j.ic.2017.04.001⟩. ⟨hal-01785464⟩

Share

Metrics

Record views

80

Files downloads

62