{"entities":{"Q6946028":{"pageid":21179745,"ns":120,"title":"Item:Q6946028","lastrevid":84093041,"modified":"2026-05-09T21:28:27Z","type":"item","id":"Q6946028","labels":{"en":{"language":"en","value":"Point-free calculational proofs and program derivation in linear algebra using a graphical syntax"}},"descriptions":{"en":{"language":"en","value":"scientific article; zbMATH DE number 8077027"}},"aliases":{},"claims":{"P31":[{"mainsnak":{"snaktype":"value","property":"P31","hash":"fd5912e4dab4b881a8eb0eb27e7893fef55176ad","datavalue":{"value":{"entity-type":"item","numeric-id":56887,"id":"Q56887"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$106C7D9C-CCEC-45E5-8A75-73D2AFD7B512","rank":"normal"}],"P159":[{"mainsnak":{"snaktype":"value","property":"P159","hash":"db21cf342845e04e7dc96aeb9f2cc79f98c510c0","datavalue":{"value":{"text":"Point-free calculational proofs and program derivation in linear algebra using a graphical syntax","language":"en"},"type":"monolingualtext"},"datatype":"monolingualtext"},"type":"statement","id":"Q6946028$45F0B9B7-E882-4771-83A2-27833179037D","rank":"normal"}],"P27":[{"mainsnak":{"snaktype":"value","property":"P27","hash":"53cacc6291c3c2d68d357cb35c0fdae9a8f040da","datavalue":{"value":"10.1017/S0956796825000085","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6946028$73979998-D231-4DF9-8657-1C24F462A3DE","rank":"normal"}],"P16":[{"mainsnak":{"snaktype":"value","property":"P16","hash":"0f7794ea5967807e06af11ef252ada7dac427ed9","datavalue":{"value":{"entity-type":"item","numeric-id":6946026,"id":"Q6946026"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$586ABF2D-47D0-43A0-A31E-1BD31265AAA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"dc9576b1b050880f5d2d3d3baf62d1adbefa84a8","datavalue":{"value":{"entity-type":"item","numeric-id":6828819,"id":"Q6828819"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$16CED91C-F4AF-48A1-984C-C71190571DDC","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P16","hash":"b79a3ea63abf3f5f19e4ed74a1a449cdbdcff8db","datavalue":{"value":{"entity-type":"item","numeric-id":6946027,"id":"Q6946027"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$8922C1E8-547D-429A-8CE3-6181F3B19735","rank":"normal"}],"P200":[{"mainsnak":{"snaktype":"value","property":"P200","hash":"c0cefd96801130048cf3f8ae21032b5cf52d744d","datavalue":{"value":{"entity-type":"item","numeric-id":2713363,"id":"Q2713363"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$C6576E7D-6F2B-4479-824D-E4D013E6D9A4","rank":"normal"}],"P28":[{"mainsnak":{"snaktype":"value","property":"P28","hash":"409b2c66c2e51a361b4c6c55661a919293a8bf4a","datavalue":{"value":{"time":"+2025-08-07T00:00:00Z","timezone":0,"before":0,"after":0,"precision":11,"calendarmodel":"http://www.wikidata.org/entity/Q1985727"},"type":"time"},"datatype":"time"},"type":"statement","id":"Q6946028$6F7A4AE3-E819-40E9-8413-B1D8414F4E8F","rank":"normal"}],"P1448":[{"mainsnak":{"snaktype":"value","property":"P1448","hash":"fe610569ba1ca3ca631ab86877341954e33ae222","datavalue":{"value":"\\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).","type":"string"},"datatype":"string"},"type":"statement","id":"Q6946028$515529D8-2396-4924-BB59-CF606D5724BD","rank":"normal"}],"P1447":[{"mainsnak":{"snaktype":"value","property":"P1447","hash":"50a4d88aaef452ee91d36bc895e7495d5ed6f713","datavalue":{"value":{"entity-type":"item","numeric-id":195143,"id":"Q195143"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$A67B4521-19A4-43DA-B5B0-B2C5660CC8A2","rank":"normal"}],"P226":[{"mainsnak":{"snaktype":"value","property":"P226","hash":"e4ea2daeca0cfefc07be3dd0f659dafac4cea2cd","datavalue":{"value":"18M30","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6946028$B8E8C8AA-DC7C-4B46-9115-8BA3DAC3F00F","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"ba5f7486cfb64f062d1b1d8e48f356198d5bc8e7","datavalue":{"value":"15A03","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6946028$D8C0BEA8-D3B3-4715-A29F-F74FBCA5D560","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"80931d057452ecc032f2d5088e7a41d514d934e3","datavalue":{"value":"18B10","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6946028$D6401211-2A75-4776-BFA9-93BF449BAE5D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"1018b98c6156b55756b9026efc9ed157beaf4774","datavalue":{"value":"18F70","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6946028$012275FF-275B-47D0-9640-D049D37207E2","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P226","hash":"40d293f5d2161e80872b42afb12a3fc45e5d1401","datavalue":{"value":"68Q55","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6946028$106BF25A-3083-4D43-81B7-CED43E2ACA81","rank":"normal"}],"P1451":[{"mainsnak":{"snaktype":"value","property":"P1451","hash":"94be02e4a651e8fa08706d5d750d4ace4436a89a","datavalue":{"value":"8077027","type":"string"},"datatype":"external-id"},"type":"statement","id":"Q6946028$D50865B5-55DA-4E5B-BF9B-1835404C5D16","rank":"normal"}],"P163":[{"mainsnak":{"snaktype":"value","property":"P163","hash":"45fcd4163b5f33e6e8c784f5522d7246c0a1a61e","datavalue":{"value":{"entity-type":"item","numeric-id":57056,"id":"Q57056"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$1D31D354-9133-431A-85C7-A581F6EFDC07","rank":"normal"}],"P1460":[{"mainsnak":{"snaktype":"value","property":"P1460","hash":"57f7fea50d2ce1b39b695c4a1313582eed405e38","datavalue":{"value":{"entity-type":"item","numeric-id":5976449,"id":"Q5976449"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$BC3D28A6-0033-447A-A121-E1B66B01F5DF","rank":"normal"}],"P223":[{"mainsnak":{"snaktype":"value","property":"P223","hash":"9db3c554db910906653b6d9583277fc79f2826ff","datavalue":{"value":{"entity-type":"item","numeric-id":774568,"id":"Q774568"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$052DBDC6-E136-4625-BB53-1823DFFD21F8","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"3eada7cfb9aa54652b8d3d79593803045e4b0c6d","datavalue":{"value":{"entity-type":"item","numeric-id":4356368,"id":"Q4356368"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$A11A21E2-3026-4562-9ED9-EC43808E282B","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"bbcb0a63005ad482c443e708ed4d6184dc02a7aa","datavalue":{"value":{"entity-type":"item","numeric-id":5261936,"id":"Q5261936"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$F6F1CB18-4B29-434B-8117-65EF3EEDF9E7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fa7326bd7714e250016f9793b37057d5c154ce69","datavalue":{"value":{"entity-type":"item","numeric-id":2225513,"id":"Q2225513"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$AAA215DD-BD2D-4109-ACB1-50D164F1C365","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"615c6a5aa369884a3c84be030981bd94d2f29ba3","datavalue":{"value":{"entity-type":"item","numeric-id":5496609,"id":"Q5496609"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$E6DD8A8E-C163-462B-83D4-043E41E5DB56","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"825ab4c172520052e5230110b703709aa8296785","datavalue":{"value":{"entity-type":"item","numeric-id":4885873,"id":"Q4885873"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$0DA31A86-CF9F-480F-80B3-84CC83511E5A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f1a449dc83ec97757d0d43544fe4421fb729c11","datavalue":{"value":{"entity-type":"item","numeric-id":5111638,"id":"Q5111638"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$23937F13-9FF8-4717-8B1E-F6D8628B1D6E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"163216dfc1f07a337d4e9acb72e1d7ba4d2310c5","datavalue":{"value":{"entity-type":"item","numeric-id":6654524,"id":"Q6654524"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$DEAC898C-AF34-4DBD-A98F-5FC5801D2BA7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"632ba73945ea4bac93467775839f31b82ba68fbd","datavalue":{"value":{"entity-type":"item","numeric-id":3190134,"id":"Q3190134"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$F3EB1285-3FD9-4BAF-ACE5-A9B02FA45B25","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"ba96f83ee5a3db35621065d31d4ce8dbdf49f7bc","datavalue":{"value":{"entity-type":"item","numeric-id":2819836,"id":"Q2819836"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$4F4F1723-BADC-48C9-B79F-DBB670C77F96","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2f5a1b23fcfd1cecde1b1c86efcb35bd03b2b321","datavalue":{"value":{"entity-type":"item","numeric-id":308156,"id":"Q308156"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$6A890F87-36C3-4C51-A336-27FC2DF6334C","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"fd51c3c41da2eaa6b1f56306d51915860a1708c3","datavalue":{"value":{"entity-type":"item","numeric-id":1098929,"id":"Q1098929"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$60ACB548-8557-4A57-97EA-67CA372C8C11","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"956ba5ee42e993010744e9428d010f5738fc442e","datavalue":{"value":{"entity-type":"item","numeric-id":5682834,"id":"Q5682834"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$05DEE223-6288-4714-ACC1-DCD423D83610","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"678fa2b9bbf2be640669ae4f7b96d06207f2ae79","datavalue":{"value":{"entity-type":"item","numeric-id":3838080,"id":"Q3838080"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$17C41088-E277-4EE5-96AD-BC021C8CAA9D","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"841a0435e587d7154f2b4d89f458f8ce704d5c22","datavalue":{"value":{"entity-type":"item","numeric-id":5347290,"id":"Q5347290"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$264C4C2B-8EC5-4C47-A4F6-07A18C4AD8DB","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7f97e95be859e33663b52106e626b60cd96dc530","datavalue":{"value":{"entity-type":"item","numeric-id":3088000,"id":"Q3088000"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$1FB15F81-3370-4E7A-80FA-C071F973FCE7","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"f3b15183e9c12d6797dea3eae200a58c3f74f918","datavalue":{"value":{"entity-type":"item","numeric-id":6038723,"id":"Q6038723"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$C51EA49E-286A-46E8-8A7A-B95409C6504A","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"29f607db4141499ef8bfa5726ceb08483e241870","datavalue":{"value":{"entity-type":"item","numeric-id":3156500,"id":"Q3156500"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$AF695E01-DD44-4E31-84E9-7B8BB0511297","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"4a172e48c61bbb704608cbf2fc0bf84a51a3ff5e","datavalue":{"value":{"entity-type":"item","numeric-id":5735219,"id":"Q5735219"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$77EF5760-1DE2-4CCA-A4EB-BE8141A1E44E","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"2696b7d5f19eb9f1b55540dd9cf1a79ddbf18186","datavalue":{"value":{"entity-type":"item","numeric-id":1683699,"id":"Q1683699"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$D2CDE8F3-CD31-4A29-A482-70C3391503DA","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"7ac1fcf052589745ac72ae23fbc9d5d1dfa38def","datavalue":{"value":{"entity-type":"item","numeric-id":3000922,"id":"Q3000922"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$FCF3EABC-392A-4985-9118-61584CB697AE","rank":"normal"},{"mainsnak":{"snaktype":"value","property":"P223","hash":"13c8aead03672358c34bd8d79cf388d54415f0ea","datavalue":{"value":{"entity-type":"item","numeric-id":6629457,"id":"Q6629457"},"type":"wikibase-entityid"},"datatype":"wikibase-item"},"type":"statement","id":"Q6946028$BB2D1AFF-6502-408E-A8A8-25A522610228","rank":"normal"}]},"sitelinks":{"mardi":{"site":"mardi","title":"Point-free calculational proofs and program derivation in linear algebra using a graphical syntax","badges":[],"url":"https://portal.mardi4nfdi.de/wiki/Point-free_calculational_proofs_and_program_derivation_in_linear_algebra_using_a_graphical_syntax"}}}}}