Towards a linear algebra of programming

Abstract

The Algebra of Programming (AoP) is a discipline for programming from specifications using relation algebra. Specification vagueness and nondeterminism are captured by relations. (Final) implemen- tations are functions. Probabilistic functions are half way between relations and functions: they express the propensity, or like- lihood of ambiguous, multiple outputs. This paper puts forward a basis for a Linear Algebra of Programming (LAoP) extending standard AoP towards probabilistic functions. Because of the quantitative essence of these functions, the allegory of binary relations which supports the AoP has to be extended. We show that, if one restricts to discrete probability spaces, categories of matrices provide adequate support for the extension, while preserving the pointfree reasoning style typical of the AoP.