Isabelle/HOL

Se ha publicado un artículo de automatización del razonamiento en Isabelle/HOL titulado Deriving comparators and show functions in Isabelle/HOL.

Sus autores son Christian Sternagel y René Thiemann (del Computational Logic Research Group en la Universidad de Innsbruck, Austria).

Su resumen es

We present an Isabelle/HOL development that allows for the automatic generation of certain operations for user-defined datatypes. Since the operations are defined within the logic, they are applicable for code generation. Triggered by the demand to provide readable error messages as well as to access efficient data structures like sorted trees in generated code, we provide show functions that compute the string representation of a given value, comparators that yield linear orders, and hash functions. Moreover, large parts of the employed machinery should be reusable for other operations like read functions, etc.

In contrast to similar mechanisms, like Haskell’s “deriving,” we do not only generate definitions, but also prove some desired properties, e.g., that a comparator indeed orders values linearly. This is achieved by a collection of tactics that discharge the corresponding proof obligations automatically.

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

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.

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.

Se ha publicado un artículo de automatización del razonamiento formalizado en Isabelle/HOL Stream fusion for Isabelle’s code generator.

Sus autores son Andreas Lochbihler y Alexandra Maximova (del Information Security Group en la Escuela Politécnica Federal de Zúrich, Suiza).

Su resumen es

Stream fusion eliminates intermediate lists in functional code. We formalise stream fusion for finite and coinductive lists in Isabelle/HOL and implement the transformation in the code preprocessor. Our initial results show that optimisations during code extraction can boost the performance of the generated code, but the transformation requires further engineering to be usable in practice.

Su contenido es un resumen de la tesis de Máster Stream Fusion for Isabelle’s Code Generator realizada por Alexandra Maximova y dirigida por Andreas Lochbihler.

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 Isabelle se encuentra aquí.