一句话：展示图形线性代数如何以无点计算式风格统一处理矩阵、向量空间和线性关系，并推导算法与性质。
本文是一篇理论珍珠，探讨如何用图形线性代数进行无点、关系式与计算式的推理。传统线性代数以向量空间和线性变换为对象，但要以无点方式有效处理子空间并不方便。作者将二者统一为线性关系，并采用关系语义与二维 string diagram 图形语法来表示和演算。这样，许多算法和性质不必仅作事后验证，而可从关系语义中计算式地推导出来。文中通过求逆、从隐式基切换到显式基（求解齐次线性系统）、交换引理以及 Zassenhaus 算法等例子展示该方法。
Abstract 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’ algorithm.
@article{MotaPM25,
title = {Point-free calculational proofs and program derivation in linear algebra using a graphical syntax},
author = {JÚLIA DE ARAÚJO MOTA and JOÃO A. PAIXÃO and LUCAS RUFINO MARTELOTTE},
journal = {Journal of Functional Programming},
volume = {35},
year = {2025},
doi = {10.1017/s0956796825000085}
}