Reseña

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Generalizing a mathematical analysis library in Isabelle/HOL.

Sus autores son Jesús Aransay y Jose Divasón de la Universidad de la Rioja.

Su resumen es

The HOL Multivariate Analysis Library (HMA) of Isabelle/HOL is focused on concrete types such as R, C and R n and on algebraic structures such as real vector spaces and Euclidean spaces, represented by means of type classes. The generalization of HMA to more abstract algebraic structures is something desirable but it has not been tackled yet. Using that library, we were able to prove the Gauss-Jordan algorithm over real matrices, but our interest lied on generating verified code for matrices over arbitrary fields, greatly increasing the range of applications of such an algorithm. This short paper presents the steps that we did and the methodology that we devised to generalize such a library, which were successful to generalize the Gauss-Jordan algorithm to matrices over arbitrary fields.

El trabajo se presentará en el NFM 2015 (The 7th NASA Formal Methods Symposium).

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre teoría de conjuntos titulado A formalisation of finite automata using hereditarily finite sets

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

Hereditarily finite (HF) set theory provides a standard universe of sets, but with no infinite sets. Its utility is demonstrated through a formalisation of the theory of regular languages and finite automata, including the Myhill-Nerode theorem and Brzozowski’s minimisation algorithm. The states of an automaton are HF sets, possibly constructed by product, sum, powerset and similar operations.

El código de las correspondientes teorías en Isabelle se encuentra aquí.

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado QR decomposition.

Sus autores son Jose Divasón y Jesús Aransay (de la Universidad de la Rioja).

Su resumen es

QR decomposition is an algorithm to decompose a real matrix A into the product of two other matrices Q and R, where Q is orthogonal and R is invertible and upper triangular. The algorithm is useful for the least squares problem; i.e., the computation of the best approximation of an unsolvable system of linear equations. As a side-product, the Gram-Schmidt process has also been formalized. A refinement using immutable arrays is presented as well. The development relies, among others, on the AFP entry Implementing field extensions of the form Q{sqrt(b)}” by René Thiemann, which allows execution of the algorithm using symbolic computations. Verified code can be generated and executed using floats as well.

El trabajo se ha publicado la semana pasada en The Archive of Formal Proofs

El código de las correspondientes teorías en Isabelle se encuentra aquí.

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre álgebra lineal titulado Echelon form.

Sus autores son Jose Divasón y Jesús Aransay (de la Universidad de la Rioja).

Su resumen es

We formalize an algorithm to compute the Echelon Form of a matrix. We have proved its existence over Bézout domains and made it executable over Euclidean domains, such as the integer ring and the univariate polynomials over a field. This allows us to compute determinants, inverses and characteristic polynomials of matrices. The work is based on the HOL-Multivariate Analysis library, and on both the Gauss-Jordan and Cayley-Hamilton AFP entries. As a by-product, some algebraic structures have been implemented (principal ideal domains, Bézout domains, …). The algorithm has been refined to immutable arrays and code can be generated to functional languages as well.

El trabajo se ha publicado la semana pasada en The Archive of Formal Proofs

El código de las correspondientes teorías en Isabelle se encuentra aquí.