Formalisation and execution of Linear Algebra: theorems and algorithms stars

  1. Divasón Mallagaray, Jose
Dirixida por:
  1. Jesús María Aransay Azofra Director
  2. Julio Rubio García Director

Universidade de defensa: Universidad de La Rioja

Fecha de defensa: 20 de xuño de 2016

Tribunal:
  1. Francis Sergeraert Presidente/a
  2. Laureano Lambán Pardo Secretario
  3. Lawrence C. Paulson Vogal
Tese doutoral con
  1. Mención internacional
Departamento:
  1. Matemáticas y Computación
Programa de doutoramento:
  1. Programa Oficial de Doctorado en Ingeniería Informática

Tipo: Tese

Repositorio institucional: lock_openAcceso aberto Editor

Resumo

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.