Matrices as arrows: why categories of matrices matter

Abstract

Due to an expanding dematerialization process, computing devices are pervasive and play vital roles in our everyday. Furthermore, society’s dependence on this technology is spiraling, which turns the dependable word the most important adjective among the computer science community that is responsible for the development and programming of such devices’ behavior. From the side of mathematics, linear algebra (LA) is catching the attention of the community because it smooths the difficulties imposed by the task of exploring the parallelism and complexity available in current computing devices and networks. Less widespread but relevant on a different register is category theory (CT), a branch of mathematics focusing on the interaction of mathematical concepts as arrows, which is used to type and reason algebraically about computing systems. Both mathematical approaches help in obtaining dependability: while one ensures the best execution time/resource usage, the other asserts behavioral correctness. The fact that the LA concept of a matrix is amenable to arrow abstraction has been by and large ignored by mathematicians and computer scientists. Categories of matrices (Mat) are mentioned just in passing in the curricula, contrarily to the cases of the category of relations, Rel, which establishes foundations for data representation and transformation and the category of sets, Set, used to reason about functional programs. Research-wise, and except for a few papers, the intersection of linear algebra and category theory is forgotten in the conundrum of theoretical formalisms. To the general professional and in common matrix languages such as e.g.MATLAB vernacular, a matrix is just a rectangle of numbers, thus neglecting the implicit algebraic type richness. The ultimate the goal of this dissertation is to integrate the forgotten categories of matrices into the mainstream of computer system foundations, trying to answer the question: ``Can matrices regarded as categorial arrows improve computer science foundations and computer system design methodologies?'' Grounded on a study of the synthesis of linear algebra kernels (algorithms) in digital signal processing (DSP) from such a perspective, it is shown how general such typed matrix theory is and how it expands to other domains such as, for instance, quantitative data aggregation in data-mining. The study of the category of matrices over a field leads to a typed matrix theory where matrices are abstracted as arrows between natural numbers (dimensions) and their categorical properties, such as biproducts, monoidality and closeness, are inspected. Biproducts and type sum operators in Mat are shown to be the essence of the whole approach because they express blocked matrix algebra in a simple and effective way. They are crucial even in the definition of the Hadamard, Khatri-Rao and Kronecker products, the latter prominent in the monoidal structure that equips the type system with a multiplication. The theory is validated by refactoring the proofs of known results (e.g. Roth’s relationship and the properties of the commutation matrix) and deriving new ones. Among these, the blocked extension to matrix linearization (vectorization) is shown to be grounded on a self-adjunction in the category. This approach enables the calculation of algorithms implementing matrix multiplication, the central operation of matrix algebra, ranging from its divide-and-conquer to vectorized implementation. Known algorithms such as e.g. Gaussian elimination are generalized blockwise by relying on the biproduct’s calculational properties. Expanding the traditional scope of application of linear algebra, the crosstabulation, cube and other constructs central to online analytical processing (OLAP) are given as case studies in the ‘‘do it in typed linear algebra’’ flavour of the dissertation. This shows how to generalize database relations from Rel to quantitative relations, i.e. typed matrices in Mat. Biproduct and type multiplication play the major role in their capturing data stacking and pairing. The end result is a calculus for OLAP which offers a new approach to the synthesis of parallel OLAP operations and which allows the proof of properties such as cross-tab incremental construction that one can hardly find elsewhere. As a whole, the dissertation helps in breaking the frontier between disjoint knowledge areas through mathematical abstraction. A number of practical applications are within reach, as is the case of implementing biproduct-based type checkers for computer algebra systems such as MATLAB and obtaining parallel OLAP systems ‘‘for free’’ based on solid aggregation/parallelization theories.

Devido a um expansivo processo de desmaterialização, os dispositivos de computa ção pululam e desempenham um papel vital no nosso dia-a-dia. Além disso, assistimos a um ritmo crescente de dependência desta tecnologia por parte da sociedade, o que fez com que a palavra confiabilidade se tornasse num adjetivo importante dentro da comunidade responsável pelo desenvolvimento e programação do comportamento destes dispositivos. Do lado da matemática, a álgebra linear (AL) tem chamado a atenção da comunidade porque suaviza os problemas impostos pela tarefa de explorar o paralelismo e a complexidade presentes nos dispositivos e redes modernas. Menos difundida, mas relevante num registo diferente está a teoria de categorias (TC), uma disciplina cujo foco é a interação entre conceitos matemáticos, modelando os artefactos matemáticos como setas, que é usada para escrever e raciocinar algebricamente sobre sistemas de computação. Ambas as abordagens matemáticas ajudam na obtenção de confiabilidade: enquanto uma garante o melhor tempo de execução/aproveitamento de recursos, a outra garante a correção do comportamento. O fato de que o conceito de matriz na AL ser passível de abstração por uma tal seta tem sido em grande parte ignorado pelos matemáticos e cientistas da computação. As categorias de matrizes são mencionadas apenas de passagem nos currículos, ao contrário dos casos da categoria de relações, Rel, que estabelece as bases para representação e transformação de dados e da categoria dos conjuntos, Set, que modela programas funcionais. Ao nível da investigação, com algumas exceções, a intersecção da álgebra linear e da teoria de categorias é esquecida na teia de formalismos teóricos. Para o profissional comum e nos sistemas que suportam o cálculo de matrizes, e.g.MATLAB, uma matriz é apenas um retângulo de números, negligenciando assim a riqueza algébrica implícita no tipo . O objetivo final desta dissertação é integrar as esquecidas categorias de matrizes no âmago dos fundamentos dos sistemas de computação, tentando responder à pergunta: ‘‘Pode a visão de matrizes como setas categoriais melhorar as fundações das ciências da computação e das metodologias do design destes sistemas?’’ Partindo do estudo da síntese de algoritmos de AL em processamento de sinal digital (DSP) nesta perspetiva, é mostrado como essa teoria de matrizes tipadas é mais geral, e como ela se expande para outros domínios, como, e.g. agregação de dados quantitativa em mineração de dados. O estudo da categoria de matrizes sobre um corpo leva a uma teoria de matrizes tipadas, onde estas são abstraídas como setas entre os números naturais (dimensões) e suas propriedades categóricas, tais como biproductos, monoidalidade e fecho, são inspecionados. É mostrado que os biproductos e operadores de soma de tipos em Mat são a essência de toda a abordagem pois expressam a álgebra matricial por blocos de uma forma simples e eficaz. São cruciais até mesmo na definição do producto de Hadamard, Khatri-Rao e Kronecker, este último destacado na estrutura monoidal que equipa os tipos com uma multiplicação. A teoria é validada refazendo as provas de resultados conhecidos (e.g. relação de Roth e as propriedades da matriz de comutação) e derivando novos. Entre estes, a extensão da linearização (vectorização) de matrizes para blocos é fundamentada numa auto-adjunção na categoria. Esta abordagem permite o cálculo de algoritmos que implementam a multiplicação de matrizes, operação central da álgebra matricial, desde a sua versão de divisão e conquista à sua implementação vectorizada. Algoritmos como a eliminação de Gauss são generalizadas por blocos, usando as propriedades calculationais do biproducto. Para alargar o âmbito de aplicação da álgebra linear, as operações basilares no processamento analítico em linha (OLAP) são usadas como estudo de caso sob o mote da dissertação: ‘‘faça-o em álgebra linear tipada’’. Mostra-se como generalizar as relações das bases de dados de Rel para versões quantitativas, i.e. matrizes em Mat. O resultado final é um cálculo de OLAP que oferece uma nova forma de extrair paralelismo e que permite a prova de propriedades tais como a sua construção incremental que dificilmente se encontra noutro lugar. Emsí, a dissertação ajudaemquebrar a fronteira entre áreas do conhecimento disjuntas através da abstração matemática. Um número de aplicações práticas estão ao alcance, como é o caso da implementação de sistemas de tipos para sistemas de álgebra computacional tais comoMATLAB, baseados em biproductos, e obtenção de sistemas paralelos OLAP ‘‘grátis’’ baseada em sólidas teorias de agregação/paralelização.