Reseña: Perron-Frobenius theorem for spectral radius analysis

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Perron-Frobenius theorem for spectral radius analysis

Sus autores son

Su resumen es

The spectral radius of a matrix A is the maximum norm of all eigenvalues of A. In previous work we already formalized that for a complex matrix A, the values in A^n grow polynomially in n if and only if the spectral radius is at most one. One problem with the above characterization is the determination of all complex eigenvalues. In case A contains only non-negative real values, a simplification is possible with the help of the Perron-Frobenius theorem, which tells us that it suffices to consider only the real eigenvalues of A, i.e., applying Sturm’s method can decide the polynomial growth of A^n.

We formalize the Perron-Frobenius theorem based on a proof via Brouwer’s fixpoint theorem, which is available in the HOL multivariate analysis (HMA) library. Since the results on the spectral radius is based on matrices in the Jordan normal form (JNF) library, we further develop a connection which allows us to easily transfer theorems between HMA and JNF. With this connection we derive the combined result: if A is a non-negative real matrix, and no real eigenvalue of A is strictly larger than one, then An is polynomially bounded in n.

El trabajo se ha publicado en The Archive of Formal Proofs.

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

Reseña: Software component design with the B method: a formalization in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Software component design with the B method: a formalization in Isabelle/HOL.

Sus autores son

  • David Déharbe (del grupo ForAll (Formal Methods and Languages Laboratory) en la UFRN (Universidade Federal do Rio Grande do Norte), Brasil) y
  • Stephan Merz (del grupo VeriDis (Verification of Distributed Systems) en el INRIA Nancy & LORIA, Francia).

Su resumen es

This paper presents a formal development of an Isabelle/HOL theory for the behavioral aspects of artifacts produced in the design of software components with the B method. We first provide a formalization of semantic objects such as labelled transition systems and notions of behavior and simulation. We define an interpretation of the B method using such concepts. We also address the issue of component composition in the B method.

El trabajo se ha presentado en FACS 2015 (12th Intl. Conf. Formal Aspects of Component Software).

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

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Reseña: Formalization of a Newton series representation of polynomials

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre álgebra titulado Formalization of a Newton series representation of polynomials.

Sus autores son Cyril Cohen y Boris Djalal (del grupo Marelle en Inria Sophia Antipolis, Francia)

Su resumen es

We formalize an algorithm to change the representation of a polynomial to a Newton power series. This provides a way to compute efficiently polynomials whose roots are the sums or products of roots of other polynomials, and hence provides a base component of efficient computation for algebraic numbers. In order to achieve this, we formalize a notion of truncated power series and develop an abstract theory of poles of fractions.

El trabajo se ha presentado en el CPP 2016 (The 5th ACM SIGPLAN Conference on Certified Programs and Proofs).

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

Este artículo puede servir de lectura complementaria en los cursos de Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Reseña: A short Isabelle/HOL tutorial for the functional programmer

PorJosé A. Alonso

Se ha publicado un tutorial de razonamiento formalizado con Isabelle/HOL titulado A short Isabelle/HOL tutorial for the functional programmer.

Su autor es Thomas Genet (de la Universidad de Rennes 1, Francia).

Su resumen es

The objective of this (very) short tutorial is to help any functional programmer to quickly put its hand on Isabelle/HOL and catch a glimpse of its power. Then, if you want some more, you should refer to the extensive Isabelle/HOL tutorial and documentation available in the tool.

Este tutorial puede servir de lectura complementaria en los cursos de Lógica matemática y fundamentos, Razonamiento automático, Razonamiento asistido por ordenador y Lógica computacional y teoría de modelos.

Reseña: Fourier series formalization in ACL2(r)

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en ACL2 sobre análisis matemático titulado Fourier series formalization in ACL2(r).

Sus autores son Cuong K. Chau, Matt Kaufmann y Warren A. Hunt Jr. (de la Univ. of Texas en Austin)

Su resumen es

We formalize some basic properties of Fourier series in the logic of ACL2(r), which is a variant of ACL2 that supports reasoning about the real and complex numbers by way of non-standard analysis. More specifically, we extend a framework for formally evaluating definite integrals of real-valued, continuous functions using the Second Fundamental Theorem of Calculus. Our extended framework is also applied to functions containing free arguments. Using this framework, we are able to prove the orthogonality relationships between trigonometric functions, which are the essential properties in Fourier series analysis. The sum rule for definite integrals of indexed sums is also formalized by applying the extended framework along with the First Fundamental Theorem of Calculus and the sum rule for differentiation. The Fourier coefficient formulas of periodic functions are then formalized from the orthogonality relations and the sum rule for integration. Consequently, the uniqueness of Fourier sums is a straightforward corollary.

We also present our formalization of the sum rule for definite integrals of infinite series in ACL2(r). Part of this task is to prove the Dini Uniform Convergence Theorem and the continuity of a limit function under certain conditions. A key technique in our proofs of these theorems is to apply the overspill principle from non-standard analysis.

El trabajo se ha presentado en el ACL2 2015 (13th International Workshop on the ACL2 Theorem Prover and Its Applications).