Reseña: QR decomposition in Isabelle/HOL
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado QR decomposition.
Sus autores son Jose Divasón y Jesús Aransay (de la Universidad de la Rioja).
Su resumen es
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.
El trabajo se ha publicado la semana pasada en The Archive of Formal Proofs
El código de las correspondientes teorías en Isabelle se encuentra aquí.