PFH: Tipos de datos algebraicos en Haskell

PorJosé A. Alonso

He añadido a la colección de Ejercicios de programación funcional con Haskell la relación Tipos de datos algebraicos en Haskell en la que se estudian los tipos abstractos de datos (TAD) tantos los predefinidos (como booleanos, opcionales, pares y listas) como definidos (árboles binarios). Se definen funciones sobre los TAD y se verifican propiedades con QuickCheck (en el caso de los TAD se definen sus generadores de elementos arbitrarios).

El contenido de la relación es el siguiente
Read More “PFH: Tipos de datos algebraicos en Haskell”

Reseña: Computational logic: its origins and applications

PorJosé A. Alonso

Lawrence C. Paulson publicó en 1998 el artículo Computational logic: its origins and applications cuyo resumen es

Computational logic is the use of computers to establish facts in a logical formalism. Originating in nineteenth century attempts to understand the nature of mathematical reasoning, the subject now comprises a wide variety of formalisms, techniques and technologies. One strand of work follows the ‘logic for computable functions (LCF) approach’ pioneered by Robin Milner, where proofs can be constructed interactively or with the help of users’ code (which does not compromise correctness). A refinement of LCF, called Isabelle, retains these advantages while providing flexibility in the choice of logical formalism and much stronger automation. The main application of these techniques has been to prove the correctness of hardware and software systems, but increasingly researchers have been applying them to mathematics itself.

y su contenido es

  1. Introduction.
  2. A brief history of formal logic.
  3. Mechanized logic: the LCF tradition.
  4. A new theorem-proving architecture: Isabelle.
  5. Formalizing mathematics.
  6. Obstacles to formalizing mathematics.
  7. The way forward.

Reseña: Windmills of the minds: an algorithm for Fermat’s two squares theorem

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en HOL4 sobre teoría de números titulado Windmills of the minds: an algorithm for Fermat’s two squares theorem.

Sus autor es Hing Lun Chan (de la Australian National University en Canberra, Australia).

Su resumen es

The two squares theorem of Fermat is a gem in number theory, with a spectacular one-sentence “proof from the Book“. Here is a formalisation of this proof, with an interpretation using windmill patterns. The theory behind involves involutions on a finite set, especially the parity of the number of fixed points in the involutions. Starting as an existence proof that is non-constructive, there is an ingenious way to turn it into a constructive one. This gives an algorithm to compute the two squares by iterating the two involutions alternatively from a known fixed point.

El trabajo se presentará en el Certified Programs and Proofs (CPP) 2022 el 18 de enero de 2022.

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

Reseña: Formalizing ordinal partition relations using Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre combinatoria titulado Formalizing ordinal partition relations using Isabelle/HOL.

Sus autores son

Su resumen es

This is an overview of a formalization project in the proof assistant Isabelle/HOL of a number of research results in infinitary combinatorics and set theory (more specifically in ordinal partition relations) by Erdős–Milner, Specker, Larson and Nash-Williams, leading to Larson’s proof of the unpublished result by E.C. Milner asserting that for all m ∈ ℕ, ω^ω → (ω^ω,m). This material has been recently formalised by Paulson and is available on the Archive of Formal Proofs; here we discuss some of the most challenging aspects of the formalization process. This project is also a demonstration of working with Zermelo–Fraenkel set theory in higher-order logic.

El trabajo se ha publicado en Experimental Mathematics.

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