QR Decomposition

Jose Divasón 🌐 and Jesús Aransay 🌐

February 12, 2015

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


QR decomposition is an algorithm to decompose a real matrix A into the product of two other matrices Q and R, where Q is orthogonal and R is invertible and upper triangular. The algorithm is useful for the least squares problem; i.e., the computation of the best approximation of an unsolvable system of linear equations. As a side-product, the Gram-Schmidt process has also been formalized. A refinement using immutable arrays is presented as well. The development relies, among others, on the AFP entry "Implementing field extensions of the form Q[sqrt(b)]" by René Thiemann, which allows execution of the algorithm using symbolic computations. Verified code can be generated and executed using floats as well.


BSD License


June 18, 2015
The second part of the Fundamental Theorem of Linear Algebra has been generalized to more general inner product spaces.


Session QR_Decomposition