Reseña: Relative monads formalised

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Agda titulado Relative monads formalised

Sus autores son

Su resumen es

Relative monads are a generalisation of ordinary monads where the underlying functor need not be an endofunctor. In this paper, we describe a formalisation of the basic theory of relative monads in the interactive theorem prover and dependently typed programming language Agda. The formalisation comprises the requisite basic category theory, the central concepts of the theory of relative monads and adjunctions, which are compared to their ordinary counterparts, and two running examples from programming theory.

El trabajo se ha publicado en el Journal of Fromalized Reasoning.

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

Reseña: Certified Kruskal’s tree theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Certified Kruskal’s tree theorem

Su autor es Christian Sternagel (del Computational Logic Research Group en la Univ. de Insbruck, Austria).

Su resumen es

This article presents the first formalization of Kurskal’s tree theorem in a proof assistant. The Isabelle/HOL development is along the lines of Nash-Williams’ original minimal bad sequence argument for proving the tree theorem. Along the way, proofs of Dickson’s lemma and Higman’s lemma, as well as some technical details of the formalization are discussed.

El trabajo se ha publicado en Journal of Formalized Reasoning.

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

I1M2014: El TAD (tipo abstracto de datos) de las tablas en Haskell

PorJosé A. Alonso

En la primera parte de la clase de hoy del curso de Informática de 1º del Grado en Matemáticas se ha estudiado cómo trabajar con tablas en Haskell usando el módulo Data.Array y en la segunda parte se ha estudiado el TAD (tipo abstracto de datos) de las tablas y tres implementaciones en Haskell: como funciones, como listas de asociación y como matrices.

Una tabla (array en inglés) es una colección de elementos (valores) a los que se accede mediante sus índices<.

El contenido la segunda parte ha sido el siguiente:

  • la signatura del TAD de las tablas;
  • las propiedades del TAD de las tablas;
  • las implementaciones, en Haskell, de las tablas mediante funciones, listas de asociación y matrices y
  • la comprobación con QuickCheck de sus propiedades.

Read More “I1M2014: El TAD (tipo abstracto de datos) de las tablas en Haskell”

Reseña: Fibonacci numbers and the Stern-Brocot tree in Coq

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Fibonacci numbers and the Stern-Brocot tree in Coq.

Sus autor es José Grimm (del Marelle Team en el Inria, Sophia-Antipolis Méditerranée).

Su resumen es

In this paper, we study the representation of a number by some other numbers. For instance, an integer may be represented uniquely as a sum of powers of two; if each power of two is allowed to appear at most twice, the number of representations is s(n), a sequence studied by Dijkstra, that has many nice properties proved here with the use of the proof assistant Coq. It happens that every rational number x is uniquely the quotient s(n)/s(n+1) as noticed by Stern, and that the integer n is related to the continued fraction expansion of x. It happens that by reverting the bits on n, one gets a sequence of rational numbers with increasing denominators that goes from 1 to x and becomes nearer at each iteration; this was studied by Brocot, whence the name Stern-Brocot tree. An integer can also be represented as a sum of Fibonacci numbers; we study R(n) the number of such representations; there is uniqueness for the predecessors of Fibonacci numbers; there is also uniqueness under additional constraints (for instance, no two consecutive Fibonacci numbers can be used, or no two consecutive numbers can be omitted).

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