Formalized Linear Algebra over Elementary Divisor Rings in Coq

Abstract : This paper presents a Coq formalization of linear algebra over elementary divisor rings, that is, rings where every matrix is equivalent to a matrix in Smith normal form. The main results are the formalization that these rings support essential operations of linear algebra, the classification theorem of finitely pre-sented modules over such rings and the uniqueness of the Smith normal form up to multiplication by units. We present formally verified algorithms comput-ing this normal form on a variety of coefficient structures including Euclidean domains and constructive principal ideal domains. We also study different ways to extend Bézout domains in order to be able to compute the Smith normal form of matrices. The extensions we consider are: adequacy (i.e. the existence of a gdco operation), Krull dimension ≤ 1 and well-founded strict divisibility.
Type de document :
Article dans une revue
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2016, <10.2168/LMCS-12(2:7)2016>
Liste complète des métadonnées


https://hal.inria.fr/hal-01081908
Contributeur : Maxime Dénès <>
Soumis le : mercredi 12 novembre 2014 - 10:44:53
Dernière modification le : samedi 29 octobre 2016 - 01:05:14
Document(s) archivé(s) le : vendredi 13 février 2015 - 10:31:34

Fichier

main.author.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas de modifications 4.0 International License

Identifiants

Collections

Citation

Guillaume Cano, Cyril Cohen, Maxime Dénès, Anders Mörtberg, Vincent Siles. Formalized Linear Algebra over Elementary Divisor Rings in Coq. Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2016, <10.2168/LMCS-12(2:7)2016>. <hal-01081908>

Partager

Métriques

Consultations de
la notice

360

Téléchargements du document

214