Typing Tensor Calculus in 2-Categories (I)
This provides a foundational framework for developers and researchers in functional programming and parallel computing to formalize tensor calculus, though it is incremental as it builds on existing category theory concepts.
The paper tackles the formalization of linear algebra calculations for efficient algorithms and functional programming by representing matrices and tensors as morphisms in semiadditive 2-categories, resulting in an index-free, typed framework that handles tensors with up to four indices.
To formalize calculations in linear algebra for the development of efficient algorithms and a framework suitable for functional programming languages and faster parallelized computations, we adopt an approach that treats elements of linear algebra, such as matrices, as morphisms in the category of matrices, $\mathbf{Mat_{k}}$. This framework is further extended by generalizing the results to arbitrary monoidal semiadditive categories. To enrich this perspective and accommodate higher-rank matrices (tensors), we define semiadditive 2-categories, where matrices $T_{ij}$ are represented as 1-morphisms, and tensors with four indices $T_{ijkl}$ as 2-morphisms. This formalization provides an index-free, typed linear algebra framework that includes matrices and tensors with up to four indices. Furthermore, we extend the framework to monoidal semiadditive 2-categories and demonstrate detailed operations and vectorization within the 2-category of 2Vec introduced by Kapranov and Voevodsky.