Weighted automata as coalgebras in categories of matrices

Abstract

The evolution from non-deterministic to weighted automata represents a shift from qual- itative to quantitative methods in computer science. The trend calls for a language able to reconcile quantitative reasoning with formal logic and set theory, which have for so many years supported qualitative reasoning. Such a lingua franca should be typed, poly- morphic, diagrammatic, calculational and easy to blend with conventional notation. This paper puts forward typed linear algebra as a candidate notation for such a unifying role. This notation, which emerges from regarding matrices as morphisms of suitable categories, is put at work in describing weighted automata as coalgebras in such categories. Some attention is paid to the interface between the index-free (categorial) language of matrix algebra and the corresponding index-wise, set-theoretic notation.