Formalisation and execution of Linear Algebra: theorems and algorithms

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...

Descripción completa

Guardado en:

Detalles Bibliográficos
Autor principal:	Divasón Mallagaray, José
Otros Autores:	Aransay Azofra, Jesús María (Universidad de La Rioja)
Formato:	text (thesis)
Lenguaje:	eng
Publicado:	Universidad de La Rioja (España) 2016
Acceso en línea:	https://dialnet.unirioja.es/servlet/oaites?codigo=49993
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

id	oai-TES0000011544
record_format	dspace
spelling	oai-TES00000115442019-08-09Formalisation and execution of Linear Algebra: theorems and algorithmsDivasón Mallagaray, José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.Universidad de La Rioja (España)Aransay Azofra, Jesús María (Universidad de La Rioja)Rubio García, Julio (Universidad de La Rioja)2016text (thesis)application/pdfhttps://dialnet.unirioja.es/servlet/oaites?codigo=49993(Tesis) ISBN 978-84-697-7278-2 engLICENCIA DE USO: Los documentos a texto completo incluidos en Dialnet son de acceso libre y propiedad de sus autores y/o editores. Por tanto, cualquier acto de reproducción, distribución, comunicación pública y/o transformación total o parcial requiere el consentimiento expreso y escrito de aquéllos. Cualquier enlace al texto completo de estos documentos deberá hacerse a través de la URL oficial de éstos en Dialnet. Más información: https://dialnet.unirioja.es/info/derechosOAI \| INTELLECTUAL PROPERTY RIGHTS STATEMENT: Full text documents hosted by Dialnet are protected by copyright and/or related rights. This digital object is accessible without charge, but its use is subject to the licensing conditions set by its authors or editors. Unless expressly stated otherwise in the licensing conditions, you are free to linking, browsing, printing and making a copy for your own personal purposes. All other acts of reproduction and communication to the public are subject to the licensing conditions expressed by editors and authors and require consent from them. Any link to this document should be made using its official URL in Dialnet. More info: https://dialnet.unirioja.es/info/derechosOAI
institution	DialNet
collection	DialNet
language	eng
description	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.
author2	Aransay Azofra, Jesús María (Universidad de La Rioja)
author_facet	Aransay Azofra, Jesús María (Universidad de La Rioja) Divasón Mallagaray, José
format	text (thesis)
author	Divasón Mallagaray, José
spellingShingle	Divasón Mallagaray, José Formalisation and execution of Linear Algebra: theorems and algorithms
author_sort	Divasón Mallagaray, José
title	Formalisation and execution of Linear Algebra: theorems and algorithms
title_short	Formalisation and execution of Linear Algebra: theorems and algorithms
title_full	Formalisation and execution of Linear Algebra: theorems and algorithms
title_fullStr	Formalisation and execution of Linear Algebra: theorems and algorithms
title_full_unstemmed	Formalisation and execution of Linear Algebra: theorems and algorithms
title_sort	formalisation and execution of linear algebra: theorems and algorithms
publisher	Universidad de La Rioja (España)
publishDate	2016
url	https://dialnet.unirioja.es/servlet/oaites?codigo=49993
work_keys_str_mv	AT divasonmallagarayjose formalisationandexecutionoflinearalgebratheoremsandalgorithms
_version_	1718346650249854976

Formalisation and execution of Linear Algebra: theorems and algorithms

Ejemplares similares