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.\N\NIt 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).