Point-free calculational proofs and program derivation in linear algebra using a graphical syntax (Q6946028)

\textit{H. D. Macedo} and \textit{J. N. Oliveira} [Sci. Comput. Prgram. 78, No. 11, 2160--2191 (2013; \url{doi:10.1016/j.scico.2012.07.012})] achieved point-free calculational reasoning in linear algebra by presenting the fundamental laws of matrix algebra as rewriting rules. The authors showed how blocked matrix notation permits point-free equational reasoning and algorithm derivation in matrix algebra. Their approach makes use of the rich biproduct structure of the category \textsf{FinVect}\(_{k}\), whose arrows are linear transformations. Despite its efficacy, subspaces appear only at the object level in, whereas arrows exclusively represent linear transformations. It is well known that when one wants point-free reasoning about relations, such as in relational algebra, it is a good idea to use the category of relations (\textsf{Rel}) in place of the category of functions (\textsf{Set}) [\textit{R. Bird} and \textit{O. de Moor}, NATO ASI Ser., Ser. F, Comput. Syst. Sci. 152, 167--203 (1996; Zbl 0847.68014)]. This paper aims to showcase an approach for linear algebra as a natural extension of the ideas of Macedo and Oliveira, where the main object of study is that of \textit{linear relation} [\textit{R. Arens}, Pac. J. Math. 11, 9--23 (1961; Zbl 0102.10201); \textit{S. MacLane}, Proc. Natl. Acad. Sci. USA 47, 1043--1051 (1961; Zbl 0123.01102)]. The authors give proofs by making use of string diagrams, which are popular objects among category theorists, and are essentially formally defined drawings with certain rules for combining them [\textit{P. Selinger}, Lect. Notes Phys. 813, 289--355 (2011; Zbl 1217.18002); \textit{J. C. Baez} and \textit{J. Erbele}, Theory Appl. Categ. 30, 836--881 (2015; Zbl 1316.18009)]. It is well known that string diagrams are a good tool for point-free reasoning and type-checking. Their graphical 2d-syntax allows one to omit parentheses around the two ways of composing relations. Their use in linear algebra has recently been explored by Zanasi [\textit{F. Zanasi}, ``Interacting Hopf algebras: the theory of linear systems'', Preprint, \url{arXiv:1805.03032}], who developed what is called graphical linear algebra (GLA).