{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:14:30Z","timestamp":1750306470568,"version":"3.41.0"},"reference-count":34,"publisher":"Cambridge University Press (CUP)","license":[{"start":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:00:00Z","timestamp":1750204800000},"content-version":"unspecified","delay-in-days":168,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["cambridge.org"],"crossmark-restriction":true},"short-container-title":["J. Funct. Prog."],"published-print":{"date-parts":[[2025]]},"abstract":"<jats:title>Abstract<\/jats:title>\n\t  <jats:p>This theoretical pearl shows how a graphical, relational, point-free, and calculational approach to linear algebra, known as graphical linear algebra, can be used to reason not only about matrices (and matrix algebra, as can be found in the literature) but also vector spaces and more generally linear relations. Linear algebra is usually seen as the study of vector spaces and linear transformations. However, to reason effectively with subspaces in a point-free and calculational manner, both can be generalized to an unifying concept: linear relations, much like relational algebra. While the semantics is relational, the syntax is graphical and uses string diagrams, 2-dimensional formal diagrams, which represent the linear relations. Most importantly, in a number of cases, the relational semantics allows algorithms and properties to be derived calculationally instead of just verified. Our approach is to proceed primarily by examples which involve finding inverses, switching from an implicit basis to an explicit basis (solving a homogeneous linear system), exploring both the exchange lemma and the Zassenhaus\u2019 algorithm.<\/jats:p>","DOI":"10.1017\/s0956796825000085","type":"journal-article","created":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:47:07Z","timestamp":1750225627000},"update-policy":"https:\/\/doi.org\/10.1017\/policypage","source":"Crossref","is-referenced-by-count":0,"title":["Point-free calculational proofs and program derivation in linear algebra using a graphical syntax"],"prefix":"10.1017","volume":"35","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-9547-9629","authenticated-orcid":false,"given":"J\u00daLIA DE ARA\u00daJO","family":"MOTA","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1610-9022","authenticated-orcid":false,"given":"JO\u00c3O A.","family":"PAIX\u00c3O","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0009-2402-7949","authenticated-orcid":false,"given":"LUCAS RUFINO","family":"MARTELOTTE","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2025,6,18]]},"reference":[{"key":"S0956796825000085_ref14","doi-asserted-by":"publisher","DOI":"10.1090\/memo\/0134"},{"key":"S0956796825000085_ref33","unstructured":"Wikipedia contributors. (2023) Zassenhaus algorithm \u2014 Wikipedia, the free encyclopedia. [Online; accessed 16-November-2023]."},{"key":"S0956796825000085_ref2","volume-title":"Undergraduate Texts in Mathematics","author":"Axler","year":"1997"},{"key":"S0956796825000085_ref7","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-61455-2_12"},{"key":"S0956796825000085_ref23","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2017.09.003"},{"key":"S0956796825000085_ref8","unstructured":"Bonchi, F. , Holland, J. , Pavlovic, D. & Sobocinski, P. (2017) Refinement for signal flow graphs. In 28th International Conference on Concurrency Theory (CONCUR 2017), Dagstuhl, Germany. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, pp. 24:1\u201324:16."},{"key":"S0956796825000085_ref10","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44584-6_30"},{"key":"S0956796825000085_ref17","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-22863-6_10"},{"key":"S0956796825000085_ref27","doi-asserted-by":"crossref","unstructured":"Selinger, P. (2011) A survey of graphical languages for monoidal categories. In New Structures for Physics, pp. 289\u2013355.","DOI":"10.1007\/978-3-642-12821-9_4"},{"key":"S0956796825000085_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2016.06.002"},{"key":"S0956796825000085_ref34","unstructured":"Zanasi, F. (2015) Interacting Hopf Algebras: The Theory of Linear Systems. PhD Thesis. Ecole Normale Sup\u00e9rieure de Lyon."},{"key":"S0956796825000085_ref4","doi-asserted-by":"publisher","DOI":"10.1007\/s11075-020-00921-w"},{"key":"S0956796825000085_ref6","doi-asserted-by":"publisher","DOI":"10.4169\/amer.math.monthly.121.07.644"},{"key":"S0956796825000085_ref1","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1961.11.9"},{"key":"S0956796825000085_ref30","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-57228-9_9"},{"key":"S0956796825000085_ref9","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2019.8785877"},{"key":"S0956796825000085_ref19","first-page":"147","article-title":"Composing props","volume":"13","author":"Lack","year":"2004","journal-title":"Theory Appl. Categ."},{"key":"S0956796825000085_ref32","unstructured":"Vaswani, A. , Shazeer, N. , Parmar, N. , Uszkoreit, J. , Jones, L. , Gomez, A. N. , Kaiser, L. & Polosukhin, I. (2023) Attention is all you need."},{"key":"S0956796825000085_ref18","doi-asserted-by":"publisher","DOI":"10.1017\/9781009317825"},{"key":"S0956796825000085_ref11","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2676993"},{"key":"S0956796825000085_ref26","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12821-9_4"},{"key":"S0956796825000085_ref13","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(87)90121-6"},{"key":"S0956796825000085_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2022.102791"},{"key":"S0956796825000085_ref31","volume-title":"Introduction to Linear Algebra","author":"Strang","year":"2009"},{"key":"S0956796825000085_ref16","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-8348-2379-3"},{"key":"S0956796825000085_ref25","doi-asserted-by":"publisher","DOI":"10.1145\/3406088.3409019"},{"key":"S0956796825000085_ref3","first-page":"836","article-title":"Categories in control","volume":"30","author":"Baez","year":"2015","journal-title":"Theory Appl. Categ."},{"key":"S0956796825000085_ref20","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.47.7.1043"},{"key":"S0956796825000085_ref29","unstructured":"Soboci\u0144ski, P. (2015) Graphical linear algebra. Mathematical blog.[Online]. Available at: https:\/\/graphicallinearalgebra.net."},{"key":"S0956796825000085_ref22","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2012.07.012"},{"key":"S0956796825000085_ref21","volume-title":"Categories for the Working Mathematician","volume":"5","author":"Mac Lane","year":"2013"},{"key":"S0956796825000085_ref28","first-page":"1049","article-title":"Linear algebra techniques for deciding the correctness of probabilistic programs with bounded resources","author":"Sernadas","year":"2008","journal-title":"Preprint, SQIG-IT and IST-TU Lisbon"},{"key":"S0956796825000085_ref5","unstructured":"Baroni, M. & Zamparelli, R. (2010) Nouns are vectors, adjectives are matrices: Representing adjective-noun constructions in semantic space. In Proceedings of the 2010 Conference on Empirical Methods in Natural Language Processing, pp. 1183\u20131193."},{"key":"S0956796825000085_ref15","volume-title":"Chapman and Hall\/CRC Pure and Applied Mathematics","author":"Cross","year":"1998"}],"container-title":["Journal of Functional Programming"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0956796825000085","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:47:11Z","timestamp":1750225631000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0956796825000085\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025]]},"references-count":34,"alternative-id":["S0956796825000085"],"URL":"https:\/\/doi.org\/10.1017\/s0956796825000085","relation":{},"ISSN":["0956-7968","1469-7653"],"issn-type":[{"value":"0956-7968","type":"print"},{"value":"1469-7653","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025]]},"assertion":[{"value":"\u00a9 The Author(s), 2025. Published by Cambridge University Press","name":"copyright","label":"Copyright","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https:\/\/creativecommons.org\/licenses\/by\/4.0\/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.","name":"license","label":"License","group":{"name":"copyright_and_licensing","label":"Copyright and Licensing"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}],"article-number":"e13"}}