Formalisation and execution of Linear Algebra: theorems and algorithms stars

Abstract

This thesis studies the formalisation and execution of Linear Algebra algorithms in Isabelle/HOL, an interactive theorem prover. The work is based on the HOL Multivariate Analysis library, whose matrix representation has been refined to datatypes that admit a representation in functional programming languages. This enables the generation of programs from such verified algorithms. In particular, several well-known Linear Algebra algorithms have been formalised involving both the computation of matrix canonical forms and decompositions (such as the Gauss-Jordan algorithm, echelon form, Hermite normal form, and QR decomposition). The formalisation of these algorithms is also accompanied by the formal proofs of their particular applications such as calculation of the rank of a matrix, solution of systems of linear equations, orthogonal matrices, least squares approximations of systems of linear equations, and computation of determinants of matrices over Bézout domains. Some benchmarks of the generated programs are presented as well where matrices of remarkable dimensions are involved, illustrating the fact that they are usable in real-world cases. The formalisation has also given place to side-products that constitute themselves standalone reusable developments: serialisations to SML and Haskell, an implementation of algebraic structures in Isabelle/HOL, and generalisations of well-established Isabelle/HOL libraries. In addition, an experiment involving Isabelle, its logics, and the formalisation of some underlying mathematical concepts presented in Voevodsky's simplicial model for Homotopy Type Theory is presented.