Typed linear algebra for weighted (probabilistic) automata

Abstract

There is a need for a language able to reconcile the recent upsurge of interest in quantitative methods in the software sciences with logic and set theory that have been used for so many years in capturing the qualitative aspects of the same body of knowledge. Such a lingua franca should be typed, polymorphic, diagrammatic, calculational and easy to blend with traditional notation. This paper puts forward typed linear algebra (LA) as a candidate notation for such a role. Typed LA emerges from regarding matrices as morphisms of suitable categories whereby traditional linear algebra is equipped with a type system. In this paper we show typed LA at work in describing weighted (prob- abilistic) automata. Some attention is paid to the interface between the index-free language of matrix combinators and the corresponding index- wise notation, so as to blend with traditional set theoretic notation.