Point-free calculational proofs and program derivation in linear algebra using a graphical syntax
\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).
- A categorical semantics of signal flow graphs
- A survey of graphical languages for monoidal categories
- AN ALGEBRA OF ADDITIVE RELATIONS
- Cartesian bicategories. I
- Categories in control
- Extended echelon form and four subspaces
- Extension theory of formally normal and symmetric subspaces
- Full abstraction for signal flow graphs
- Graphical affine algebra
- scientific article; zbMATH DE number 2125662 (Why is no real title available?)
- scientific article; zbMATH DE number 1183904 (Why is no real title available?)
- scientific article; zbMATH DE number 1065062 (Why is no real title available?)
- scientific article; zbMATH DE number 910715 (Why is no real title available?)
- Interacting Hopf algebras
- Introducing String Diagrams
- Operational calculus of linear relations
- Point-free, set-free concrete linear algebra
- Primer of linear algebra and analytic geometry. The essentials in detail, for teacher and bachelor students. With the collaboration of Florian Quiring
- Programming from metaphorisms
- Refinement for signal flow graphs
- Towards a compositional framework for convex analysis (with applications to probability theory)
- Two algorithms for the exchange lemma
This page was built for publication: Point-free calculational proofs and program derivation in linear algebra using a graphical syntax
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6946028)
