arXiv:1308.1138cs.LO
The Vectorial $λ$-Calculus
Early discovery. Linked by one identifiable commenter. This paper is outside the main ranking; a mention is not an endorsement.
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.
Hi Michel - You're working on a GraphBLAS Postgres implementation [0] -- here's an open question I've been pondering... [0] Postgres GraphBLAS https://github.com/michelp/pggraphblas Now that we have SOTA linear algebra models for graphs [1], logic [2] and the lambda calculus [3]…
espeedView on HNParent context