Los números de Ulam en Haskell

PorJosé A. Alonso

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

PorJosé A. Alonso

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

La Lógica en las ciencias computacionales

PorJosé A. Alonso

Se ha publicado un artículo sobre la enseñanza de la lógica titulado La Lógica en las ciencias computacionales.

Su autor es Edgar Serna M. (del Instituto Tecnológico Metropolitano, Medellín (Colombia)).

Su resumen es

En este trabajo se hace un análisis a la necesidad de incluir a la lógica en los procesos formativos en Ciencias Computacionales (CS por sus siglas en inglés). Se parte de un recorrido sobre la historia de la lógica en estas ciencias, posteriormente se describe la relación y la necesidad de incluirla en los procesos formativos relacionados, y al final se analiza qué, cuándo y qué tan profundo se debería trabajar en la formación en CS. Se trata de una revisión al estado del tema y a la importancia de incluirlo en los pregrados y en los posgrados en áreas de ciencias computacionales y tecnologías de información.

El artículo se ha publicado en la Revista Educación en Ingeniería.

Proof pearl: A verified bignum implementation in x86-64 machine code

PorJosé A. Alonso

Se ha publicado un artículo de verificación formal en HOL4 titulado Proof pearl: A verified bignum implementation in x86-64 machine code.

Sus autores son

  • Magnus O. Myreen (de la Universidad de Cambridge)y
  • Gregorio Curello (de la Universidad Autónoma de Barcelona).

Su resumen es

Verification of machine code can easily deteriorate into an endless clutter of low-level details. This paper presents a case study which shows that machine-code verification does not necessarily require ghastly low-level proofs. The case study we describe is the construction of an x86-64 implementation of arbitrary-precision integer arithmetic. Compared with closely related work, our proofs are shorter and, more importantly, the reasoning is at a more convenient high level of abstraction, e.g. pointer reasoning is largely avoided. We achieve this improvement as a result of using previously developed tools, namely, a proof-producing decompiler and compiler. The work presented in this paper has been developed in the HOL4 theorem prover and the case study resulted in 700 lines of verified 64-bit x86 machine code.

El código correspondiente se encuentra aquí.

El trabajo se presentará en la CPP 2013 (3rd International Conference on Certified Programs and Proofs).

Mechanized metatheory for a λ λ-calculus with trust types

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Coq titulado Mechanized metatheory for a λ λ-calculus with trust types.

Sus autores son

Su resumen es

As computer programs become increasingly complex, techniques for ensuring trustworthiness of information manipulated by them become critical. In this work, we use the Coq proof assistant to formalise a λ λ -calculus with trust types, originally formulated by Ørbæk and Palsberg. We give formal proofs of type soundness, erasure and simulation theorems and also prove decidability of the typing problem. As a result of our formalisation a certified type checker is derived.

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

La versión final del trabajo se ha publicado en el Journal of the Brazilian Computer Society.