Los números de Ulam en Haskell

Los números de Ulam son los elementos de la sucesión u(n) definida por u(1) = 1, u(2) = 2 y, para n > 2, u(n) es el entero más pequeño que se puede escribir exactamente de una forma como suma de dos términos anteriores diferentes entre sí.

Según la definición, 3=1+2 es un número de Ulam y 4=1+3 también es un número de Ulam (la suma 4=2+2 no cuenta porque los términos previos deben ser distintos). El entero 5 no es un número de Ulam porque 5=1+4=2+3.

Los primeros términos de la sucUlam son: 1, 2, 3, 4, 6, 8, 11, 13, 16, 18, 26, 28, 36, 38, 47, 48, 53, 57, 62, 69, 72, 77, 82, 87, 97, 99.

Esta sucesión fue definida por el matemático polaco Stanislaw Ulam y
publicada en SIAM Review en 1964.

A partir de los artículos de la Wikipedia y de MathWorld sobre los números de Ulam elaborado la siguiente relación de ejercicios de Haskell para la asignatura de Informática de 1º del Grado en Matemáticas.

En la relación se presentan cuatro definiciones de los números de Ulam, se compara su eficiencia, se muestra algunas de sus propiedades terminando con los números de Ulam generalizados.
Read More “Los números de Ulam en Haskell”

Generic datatypes à la carte

Se ha publicado un artículo de automatización del razonamiento en Coq titulado Generic datatypes à la carte.

Sus autores son Steven Keuchel y Tom Schrijvers (de la Universidad de Gante, Bélgica).

Su resumen es

Formal reasoning in proof assistants, also known as mechanization, has high development costs. Building modular reusable components is a key issue in reducing these costs. A stumbling block for reuse is that inductive definitions and proofs are closed to extension. This is a manifestation of the expression problem that has been addressed by the Meta-Theory à la Carte (MTC) framework in the context of programming language meta-theory. However, MTC’s use of extensible Church-encodings is unsatisfactory.

This paper takes a better approach to the problem with datatype- generic programming (DGP). It applies well-known DGP techniques to represent modular datatypes, to build functions from functor algebras with folds and to compose proofs from proof algebras by means of induction. Moreover, for certain functionality and proofs our approach can achieve more reuse than MTC: instead of composing modular components we provide a single generic definition once and for all.

El correspondiente código en Coq se encuentra aquí.

El trabajo se presentará en el WGP 2013 (9th ACM SIGPLAN Workshop on Generic Programming).