Reseña: Higman’s lemma and its computational content

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Minlog sobre combinatoria titulado Higman’s lemma and its computational content.

Sus autores son

Su resumen es

Higman’s Lemma is a fascinating result in infinite combinatorics, with manyfold applications in logic and computer science. It has been proven several times using different formulations and methods. The aim of this paper is to look at Higman’s Lemma from a computational and comparative point of view. We give a proof of Higman’s Lemma that uses the same combinatorial idea as Nash-Williams’ indirect proof using the so-called minimal bad sequence argument, but which is constructive. For the case of a two letter alphabet such a proof was given by Coquand. Using more flexible structures, we present a proof that works for an arbitrary well-quasiordered alphabet. We report on a formalization of this proof in the proof assistant Minlog, and discuss machine extracted terms (in an extension of Gödel’s system T) expressing its computational content.

Reseña: Generalizing a mathematical analysis library in Isabelle/HOL

PorJosé A. Alonso

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

Reseña: A formalisation of finite automata using hereditarily finite sets

PorJosé A. Alonso

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

Reseña: Program verification by coinduction

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Program verification by coinduction.

Sus autores son Brandon Moore y Grigore Rosu (del Formal Systems Laboratory en la Universidad de Illinois en Urbana-Champaign).

Su resumen es

We present a program verification framework based on coinduction, which makes it feasible to verify programs directly against an operational semantics, without requiring intermediates like axiomatic semantics or verification condition generators. Specifications can be written and proved using any predicates on the state space of the operational semantics.

We implement our approach in Coq, giving a certifying language-independent verification framework. The core proof system is implemented as a single module imported unchanged into proofs of programs in any semantics. A comfortable level of automation is provided by instantiating a simple heuristic with tactics for language-specific tasks such as finding the successor of a symbolic state, and for domain-specific reasoning about the predicates used in a particular specification. This approach also smoothly allows manual assistance at points the automation cannot handle.

We demonstrate the power of our approach by verifying algorithms as complicated as Schorr-Waite graph marking, and the versatility by instantiating it for object languages in several styles of semantics. Despite the greater flexibility and generality of our approach, proof size and proof/certificate-checking time compare favorably with Bedrock, another Coq-based certifying program verification framework.

Reseña: QR decomposition in Isabelle/HOL

PorJosé A. Alonso

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