Correct by Construction Gram-Schmidt Process

• João Victor Lopez Pereira UFRJ
• Daniel Kiyoshi Hashimoto UFRJ
• Hugo Musso Gualandi UFRJ
• João Paixão UFRJ

DOI: https://doi.org/10.5753/sblp.2026.28541

Resumo

The programming languages community has developed proof techniques for reasoning about correctness and equivalence of stream programs in a concise and precise way whilst not worrying about indexes. These ideas can be applied to areas, such as linear algebra, where indexes are the gold-standard.We showcase this through the lens of the Gram-Schmidt process for producing an orthonormal basis, which is an online algorithm that can be succinctly implemented as a purely functional stream program. Our first contribution is a specification of orthogonalization as a Galois Connection. Our second contribution is a correct-by-construction derivation of the classical Gram-Schmidt algorithm directly from its specification. Our third contribution is an induction-free proof that the more numerically stable modified Gram-Schmidt algorithm is equivalent to its classical counterpart. All of our proofs are index-free, in the sense that we do not use indexes to refer to vectors in a basis nor to elements in a vector.

Palavras-chave: Streams, Linear Algebra, Equational Reasoning, Gram-Schmidt, Modified Gram-Schmidt, Galois Connection

Referências

Roland Backhouse. 2003. Program Construction: Calculating Implementations from Specifications. Wiley, Chichester, England.

Edsger Wybe Dijkstra and Willem H. J. Feijen. 1988. A Method of Programming. Addison-Wesley, Reading, MA.

Gene H. Golub and Charles F. Van Loan. 2013. Matrix Computations. JHU press, Baltimore, MD. A presentation of the Modified Gram-Schmidt algorithm and a discussion of its numerical accuracy can be found in Chapter 5.

Ralf Hinze. 2010. Concrete Stream Calculus: An Extended Study. Journal of Functional Programming 20, 5-6 (2010), 463–535. DOI: 10.1017/S0956796810000213

Graham Hutton and Mauro Jaskelioff. 2013. Representing Contractive Functions on Streams (Extended Version). Technical Report. School of Computer Science, University of Nottingham. [link]

Shin-Cheng Mu and José Nuno Oliveira. 2012. Programming from Galois Connections. The Journal of Logic and Algebraic Programming 81, 6 (2012), 680–704. DOI: 10.1016/j.jlap.2012.05.003, 12th International Conference on Relational and Algebraic Methods in Computer Science (RAMiCS 2011).

José Nuno Oliveira. 2023. Why Adjunctions Matter—A Functional Programmer Perspective. In Recent Trends in Algebraic Development Techniques, Alexandre Madeira and Manuel A. Martins (Eds.). Springer Nature Switzerland, Cham, 25–59.

Paulo Ricardo Antunes Pereira. 2023. Back to Programming from Galois Connections. Master’s thesis. Universidade do Minho.

Jan J. M. M. Rutten. 2003. Behavioural Differential Equations: A Coinductive Calculus of Streams, Automata, and Power Series. Theoretical Computer Science 308, 1–3 (2003), 1–53. DOI: 10.1016/S0304-3975(02)00895-2

Jan J. M. M. Rutten. 2005. A Coinductive Calculus of Streams. Mathematical Structures in Computer Science 15, 1 (2005), 93–147. DOI: 10.1017/S0960129504004507

Lloyd N. Trefethen and David Bau. 1997. Numerical Linear Algebra. Society for Industrial and Applied Mathematics, Philadelphia, PA. The classical and modified Gram-Schmidt algorithms are discussed in lectures 7 and 8. Their numerical stability is discussed in lecture 19.