Formalized Linear Algebra over Elementary Divisor Rings in Coq
In: EISSN: 1860-5974 ; Logical Methods in Computer Science ; https://inria.hal.science/hal-01081908 ; Logical Methods in Computer Science, 2016, ⟨10.2168/LMCS-12(2:7)2016⟩, 2016
Online
academicJournal
Zugriff:
International audience ; 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.
Titel: |
Formalized Linear Algebra over Elementary Divisor Rings in Coq
|
---|---|
Autor/in / Beteiligte Person: | Cano, Guillaume ; Cohen, Cyril ; Dénès, Maxime ; Mörtberg, Anders ; Siles, Vincent ; Université de Perpignan Via Domitia (UPVD) ; Mathematical, Reasoning and Software (MARELLE) ; Inria Sophia Antipolis - Méditerranée (CRISAM) ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; University of Pensylvania ; Göteborgs Universitet = University of Gothenburg (GU) ; Department of Computer Science and Engineering Göteborg (CSE) ; Chalmers University of Technology Göteborg ; European Project: 243847,EC:FP7:ICT,FP7-ICT-2009-C,FORMATH(2010) |
Link: | |
Zeitschrift: | EISSN: 1860-5974 ; Logical Methods in Computer Science ; https://inria.hal.science/hal-01081908 ; Logical Methods in Computer Science, 2016, ⟨10.2168/LMCS-12(2:7)2016⟩, 2016 |
Veröffentlichung: | HAL CCSD ; Logical Methods in Computer Science Association, 2016 |
Medientyp: | academicJournal |
DOI: | 10.2168/LMCS-12(2:7)2016 |
Schlagwort: |
|
Sonstiges: |
|