I1M2012: Potencias con el último dígito invariante

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado la solución con Haskell de siguiente problema

Calcular el menor número natural n, mayor que 1, tal que para cualquier número entero x se verifique que x y xⁿ terminan en el mismo dígito.

La especificación matemática del enunciado es

min {n∈ℕ | n>1 ∧ ∀x∈ℤ (U(xⁿ) = U(x))}

donde U(x) es el último dígito de x. La especificación se puede reducir a

min {n∈ℕ | n>1 ∧ ∀x∈{0,…,9} (U(xⁿ) = U(x))}

Su traducción a Haskell es

donde (ultimo x) es el último dígito de x

La solución del problema se calcula con

Se puede generalizar solP3 a una función solP3′ que calcula todos los números naturales n, mayores que 1, tales que para cualquier número entero x se verifique que x y xⁿ terminan en el mismo dígito. Para ello, basta eliminar head en la definición de solP3

El cálculo de los 20 primeros es

Se observa que forman una progresión aritmética de diferencia 4. Basándonos en esta observación se puede redefinir solP3′ como sigue

Se puede comprobar experimentalmente la conjetura definiendo la función comprobacion tal que (comprobacion n) se verifica si los n primeros elementos de solP3′ son los mismos que los de solP3”.

La comprobación para los 1000 primeros elementos es

Queda pendiente la demostración de la conjetura.

I1M2012: Números sin coprimos no primos

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas hemos comentado la solución con Haskell del problema propuesto la Olimpiada Internacional de Matemáticas (IMO) de 1978 cuyo enunciado es

Calcular todos los números naturales n < 1978 con la siguiente propiedad: Si m es un número natural, 1 < m < n, y m y n son coprimos (es decir, el máximo común divisor de m y n es 1), entonces m es un número primo.

La representación matemática del enunciado es

{n∈ℕ | n<1978, ∀m∈ℕ (1 < m < n ∧ mcd(n,m) = 1 ⟶ m es primo}

y su traducción a Haskell es

donde (primo m) se verifica si m es primo

y (factores n) es la lista de los números que dividen a n

La solución del problema se calcula con

Se puede generalizar solP2 a una función solP2′ tal que (solP2′ x) es el conjunto de los números naturales n < x tales que si m es un número natural, 1 < m < n, y m y n son coprimos, entonces m es un número primo.

Por ejemplo,

A la vista de los cálculos anteriores se conjetura que el conjunto de los números naturales n tales que si m es un número natural, 1 < m < n, y m y n son coprimos, entonces m es un número primo es [1,2,3,4,6,8,12,18,24,30].

Queda pendiente la demostración de la conjetura.

Reseña: Proof pearl – A mechanized proof of GHC’s mergesort

Se publicado un artículo de verificación en Iabelle/HOL titulado Proof pearl – A mechanized proof of GHC’s mergesort.

Su autor es Christian Sternagel (de la Univ. de la Univ. de Insbruck).

Su resumen es

We present our Isabelle/HOL formalization of GHC’s sorting algorithm for lists, proving its correctness and stability. This constitutes another example of applying a state-of-the-art poof assistant to real-world code. Furthermore, it allows users to take advantage of the formalized algorithm in generated code.

La librería estándard de GHC (The Glasgow Haskell Compiler) tiene un algoritmo de ordenación, que es una variante de la ordenación por mezcla. El objetivo del trabajo es la verificación de dicho algortimo en Isabelle/HOL, demostrando su corrección y estabilidad.

La principal característica de este trabajo es la verificación de programas eficientes. El método empleado tiene tres pasos:

  1. formalizar variantes del algoritmo que faciliten la demostración y probar todas las propiedades deseadas;
  2. formalizar variantes eficientes del algoritmo y probar su equivalencia y
  3. usar la generación de código y obtener un programa eficiente del que se tiene garantía que satisface todas las propiedades que se probaron en la formalización inicial.

La formalización es pequeña (menos de 400 líneas de código) y la mayoría de las demostraciones son automáticas. Este éxito se basa en dos principios: la generalización de los conceptos y la definición de esquemas de inducción.

El código en Isabelle/HOL de la teoría correspondiente al trabajo se encuentra en The Archive of Formal Proofs.

PeH: Piensa en Haskell (Ejercicios de programación funcional con Haskell)

He publicado la primera versión de libro Piensa en Haskell (Ejercicios de programación funcional con Haskell).

Este libros es una introducción a la programación funcional con Haskell a través de una colección de ejercicios resueltos de los cursos de Informática (del
Grado en Matemáticas) y Programación declarativa (de la Ingeniería en Informática).

Los temas correspondientes a los ejercicios del libro se encuentra en Temas de programación funcional.

El libro consta de tres partes. En la primera parte se presentan los elementos básicos de la programación funcional. En la segunda, se estudian la implementación en Haskell de tipos abstractos de datos y sus aplicaciones así como cuestiones algorítmicas. En la tercera, se presentan casos de estudios. También se han incluido dos apéndices: uno con un resumen de las funciones de Haskell utilizadas y otro con el método de Pólya para la resolución de problemas.
Read More “PeH: Piensa en Haskell (Ejercicios de programación funcional con Haskell)”

Reseña: Compiling concurrency correctly (Verifying software transactional memory)

Se ha publicado una nueva tesis de verificación con Agda: Compiling concurrency correctly (Verifying software transactional memory)

Su autor es Liyang Hu, dirigido por Graham Hutton.

La tesis se ha presentado el pasado mes de junio en la Universidad de Nottingham.

El resumen de la tesis es

Concurrent programming is notoriously difficult, but with multi-core processors becoming the norm, is now a reality that every programmer must face. Concurrency has traditionally been managed using low-level mutual exclusion locks, which are error-prone and do not naturally support the compositional style of programming that is becoming indispensable for today’s large-scale software projects.

A novel, high-level approach that has emerged in recent years is that of software transactional memory (STM), which avoids the need for explicit locking, instead presenting the programmer with a declarative approach to concurrency. However, its implementation is much more complex and subtle, and ensuring its correctness places significant demands on the compiler writer.

This thesis considers the problem of formally verifying an implementation of STM. Utilising a minimal language incorporating only the features that we are interested in studying, we first explore various STM design choices, along with the issue of compiler correctness via the use of automated testing tools. Then we outline a new approach to concurrent compiler correctness using the notion of bisimulation, implemented using the Agda theorem prover. Finally, we show how bisimulation can be used to establish the correctness of a low-level implementation of software transactional memory.