Reseña: Formalized linear algebra over elementary divisor rings in Coq
Se ha publicado un artículo de razonamiento formalizado en Coq sobre álgebra titulado Formalized linear algebra over elementary divisor rings in Coq.
Sus autores son
- Guillaume Cano del grupo Marelle en el Inria Sophia Antipolis (Francia),
- Cyril Cohen del grupo Marelle en en el Inria Sophia Antipolis (Francia),
- Maxime Dénès del grupo Marelle en en el Inria Sophia Antipolis (Francia),
- Anders Mörtberg de la Universidad de Gotemburgo (Suecia),
- Vincent Siles de la Universidad de Gotemburgo (Suecia).
Su resumen es
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 presented modules over such rings and the uniqueness of the Smith normal form up to multiplication by units. We present formally verified algorithms computing 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.
El trabajo se ha publicado en Logical Methods in Computer Science (Volume 12, Issue 2).
El código de las correspondientes teorías en Coq se encuentra aquí.