Reseña: Formalization of Shannon’s theorems

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre teoría de la información titulado Formalization of Shannon’s theorems.

Sus autores son

Su resumen es

The most fundamental results of information theory are Shannon’s theorems. These theorems express the bounds for (1) reliable data compression and (2) data transmission over a noisy channel. Their proofs are non-trivial but are rarely detailed, even in the introductory literature. This lack of formal foundations is all the more unfortunate that crucial results in computer security rely solely on information theory: this is the so-called “unconditional security”. In this article, we report on the formalization of a library for information theory in the SSReflect extension of the Coq proof-assistant. In particular, we produce the first formal proofs of the source coding theorem, that introduces the entropy as the bound for lossless compression, and of the channel coding theorem, that introduces the capacity as the bound for reliable communication over a noisy channel.

El artículo, publicado en el JAR, es una extensión del trabajo Formalization of Shannon’s Theorems in SSReflect-Coq presentado en el ITP 2012.

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: Decreasing diagrams for Church-Rosser modulo

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre reescritura titulado Decreasing diagrams for Church-Rosser modulo.

Su autor es Bertram Felgenhauer (del Computational Logic Research Group en la Universidad de Innsbruck, Austria).

Su resumen es

This theory formalizes a commutation version of decreasing diagrams for Church-Rosser modulo. The proof follows Felgenhauer and van Oostrom (RTA 2013). The theory also provides important specializations, in particular van Oostrom’s conversion version (TCS 2008) of decreasing diagrams.

We follow the development described in 1: Conversions are mapped to Greek strings, and we prove that whenever a local peak (or cliff) is replaced by a joining sequence from a locally decreasing diagram, then the corresponding Greek strings become smaller in a specially crafted well-founded order on Greek strings. Once there are no more local peaks or cliffs are left, the result is a valley that establishes the Church-Rosser modulo property.

As special cases we provide non-commutation versions and the conversion version of decreasing diagrams by van Oostrom 3. We also formalize extended decreasingness 2.

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

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: Matrices, Jordan normal forms, and spectral radius theory

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre
álgebra lineal titulado Matrices, Jordan normal forms, and spectral radius theory.

Sus autores son René Thiemann y Akihisa Yamada (del Computational Logic Group en la Universidad de Innsbruck, Austria)

Su resumen es

Matrix interpretations are useful as measure functions in termination proving. In order to use these interpretations also for complexity analysis, the growth rate of matrix powers has to examined. Here, we formalized a central result of spectral radius theory, namely that the growth rate is polynomially bounded if and only if the spectral radius of a matrix is at most one.

To formally prove this result we first studied the growth rates of matrices in Jordan normal form, and partially prove the result that every complex matrix has a Jordan normal form: we are restricted to upper-triangular matrices since we did not yet formalize the Schur decomposition.

The whole development is based on a new abstract type for matrices, which is also executable by a suitable setup of the code generator. It completely subsumes our former AFP-entry on executable matrices, and its main advantage is its close connection to the HMA-representation which allowed us to easily adapt existing proofs on determinants.

All the results have been applied to improve CeTA, our certifier to validate termination and complexity proof certificates.

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

El código de las correspondientes teorías en Isabelle 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 error-correcting codes (from Hamming to modern coding theory)

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq sobre codificación titulado Formalization of error-correcting codes (from Hamming to modern coding theory)

Sus autores son

Su resumen es

By adding redundancy to transmitted data, error-correcting codes (ECCs) make it possible to communicate reliably over noisy channels. Minimizing redundancy and (de)coding time has driven much research, culminating with Low-Density Parity-Check (LDPC) codes. At first sight, ECCs may be considered as a trustful piece of computer systems because classical results are well-understood. But ECCs are also performance-critical so that new hardware calls for new implementations whose testing is always an issue. Moreover, research about ECCs is still flourishing with papers of ever-growing complexity. In order to provide means for implementers to perform verification and for researchers to firmly assess recent advances, we have been developing a formalization of ECCs using the SSReflect extension of the Coq proof-assistant. We report on the formalization of linear ECCs, duly illustrated with a theory about the celebrated Hamming codes and the verification of the sum-product algorithm for decoding LDPC codes.

El trabajo se presentó el 25 de agosto en el ITP 2015 (The 6th conference on Interactive Theorem Proving).

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: Verified over-approximation of the diameter of propositionally factored transition systems

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre verificación titulado Verified over-approximation of the diameter of propositionally factored transition systems.

Sus autores son
+ Mohammad Abdulaziz (del Software Systems Research Group del NICTA en Camberra, Australia),
+ Charles Gretton (de la Australian National University en Camberra, Australia) y
+ Michael Norrish (del Software Systems Research Group del NICTA en Camberra, Australia)

Su resumen es

To guarantee the completeness of bounded model checking (BMC) we require a completeness threshold. The diameter of the Kripke model of the transition system is a valid completeness threshold for BMC of safety properties. The recurrence diameter gives us an upper bound on the diameter for use in practice. Transition systems are usually described using (propositionally) factored representations. Bounds for such lifted representations are calculated in a compositional way, by first identifying and bounding atomic subsystems, and then composing those results according to subsystem dependencies to arrive at a bound for the concrete system. Compositional approaches are invalid when using the diameter to bound atomic subsystems, and valid when using the recurrence diameter. We provide a novel overapproximation of the diameter, called the sublist diameter, that is tighter than the recurrence diameter. We prove that compositional approaches are valid using it to bound atomic subsystems. Those proofs are mechanised in HOL4. We also describe a novel verified compositional bounding technique which provides tighter overall bounds compared to existing bottom-up approaches.

El trabajo se presentó el 26 de agosto en el ITP 2015 (The 6th conference on Interactive Theorem Proving).

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