Menu Close

Etiqueta: Reseña

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

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

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)

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

Reseña: Formal proofs of transcendence for e and π as an application of multivariate and symmetric polynomials

Se ha publicado un artículo de razonamiento formalizado en Coq sobre teoría de números titulado Formal proofs of transcendence for e and π as an application of multivariate and symmetric polynomials.

Sus autores son

Su resumen es

We describe the formalisation in Coq of a proof that the numbers e and π are transcendental. This proof lies at the interface of two domains of mathematics that are often considered separately: calculus (real and elementary complex analysis) and algebra. For the work on calculus, we rely on the Coquelicot library and for the work on algebra, we rely on the Mathematical Components library. Moreover, some of the elements of our formalized proof originate in the more ancient library for real numbers included in the Coq distribution. The case of π relies extensively on properties of multivariate polynomials and this experiment was also an occasion to put to test a newly developed library for these multivariate polynomials.

El trabajo se presentará el 18 de enero de 2016 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í.

Reseña: A survey of interactive theorem proving

Se ha publicado un artículo sobre razonamiento formalizado titulado A survey of interactive theorem proving.

Su autor es Filip Marić (del Automated Reasoning GrOup (ARGO) en la Universidad de Belgrado, Serbia).

Su resumen es

Fully formally verified mathematics and software are long-standing aims that became practically realizable with modern computer tools. Reasoning can be reduced to several basic logical principles, and performed using specialized software, with significant automation. Although full automation is not possible, three main paradigms are represented in formal reasoning tools: (i) decision procedures for special classes of problems, (ii) complete, but potentially unterminating proof search, (iii) checking of proof-sketches given by a human user while automatically constructing simpler proof steps. In this paper, we present a survey of the third approach, embodied in modern interactive theorem provers (ITP), also called proof-assistants. These tools have been successfully developed for more than 40 years, and the current state-of-the-art tools have reached maturity needed to perform real-world large-scale formalizations of mathematics (e.g., Four-Color Theorem, Prime Number Theorem, and Feith-Thompson’s Odd Order theorem) and software correctness (e.g., substantial portions of operating systems and compilers have been verified). We discuss history of ITP, its logical foundations, main features of state-of-the-art systems, and give some details about the most prominent results in the field. We also summarize main results of the researchers from Serbia and personal results of the author.

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: Formalisation in constructive type theory of Stoughton’s substitution for the lambda calculus

Se ha publicado un artículo de razonamiento formalizado en Agda sobre metalógica titulado Formalisation in constructive type theory of Stoughton’s substitution for the lambda calculus.

Sus autores son Álvaro Tasistro, Ernesto Copello y Nora Szasz (del Grupo de Computación Teórica (Compute) en la Universidad ORT, Uruguay).

Su resumen es

In Substitution revisited, Alley Stoughton proposed a notion of (simultaneous) substitution for the Lambda calculus as formulated in its original syntax – i.e. with only one sort of symbols (names) for variables – and without identifying α-convertible terms. According to such formulation, the action of substitution on terms is defined by simple structural recursion and an interesting theory arises concerning the connection to α-conversion.

In this paper we present a formalisation of Stoughton’s work in Constructive Type Theory using the language Agda, which reaches up to the Substitution Lemma for α-conversion. The development has been quite inexpensive e.g. in labour cost, and we are able to formulate some improvements over the original presentation. For instance, our definition of α-conversion is just syntax directed and we prove it to be an equivalence relation in an easy way, whereas in Substitution revisited the latter was included as part of the definition and then proven to be equivalent to an only nearly structural definition as corollary of a lengthier development. As a result of this work we are inclined to assert that Stoughton’s is the right way to formulate the Lambda calculus in its original, conventional syntax and that it is a formulation amenable to fully formal treatment.

El trabajo se ha publicado en Electronic Notes in Theoretical Computer Science.

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

Reseña: Hofstadter’s problem for curious readers

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Hofstadter’s problem for curious readers.

Su autor es Pierre Letouzey (del grupo PPS (Preuves, Programmes et Systèmes) de la Universidad de París VII Denis Diderot, Francia).

Su resumen es

This document summarizes the proofs made during a Coq development in Summer 2015. This development investigates the function G introduced by Hofstadter in his famous “Gödel, Escher, Bach” book as well as a related infinite tree. The left/right flipped variant of this G tree has also been studied here, following Hofstadter’s “problem for the curious reader”. The initial G function is refered as sequence A005206 in OEIS, while the flipped version is the sequence A123070.

The detailed and machine-checked proofs can be found in the files of
this development and can be re-checked by running Coq version 8.4 on it. No prior knowledge of Coq is assumed here, on the contrary this document has rather been a “Coq-to-English” translation exercise for the author. Nonetheless, some proofs given in this document are still quite sketchy: in this case, the interested reader is encouraged to consult the Coq files given as references.

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: Deriving comparators and show functions in 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.

Reseña: Case of (quite) painless dependently typed programming: Fully certified merge sort in Agda

Se ha publicado un artículo de razonamiento formalizado en Agda titulado Case of (quite) painless dependently typed programming: Fully certified merge sort in Agda.

Sus autores son Ernesto Copello, Álvaro Tasistro y Bruno Bianchi (del Grupo de Computación Teórica (Compute) en la Universidad ORT, Uruguay).

Su resumen es

We present a full certification of merge sort in the language Agda. It features: termination warrant without explicit proof, no proof cost to ensure that the output is sorted, and a succinct proof that the output is a permutation of the input.

El trabajo se ha presentado en The Brazilian Symposium on Programming Languages (SBLP).

El código de las correspondientes teorías en Agda 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 Shannon’s theorems

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.