José A. Alonso

Números de Lychrel

PorJosé A. Alonso 13 agosto 201030 abril 2015

Según la Wikipedia, un número de Lychrel es un número natural para el que nunca se obtiene un capicúa mediante el proceso de invertir las cifras y sumar los dos números. Por ejemplo, los siguientes números no son números de Lychrel:

56, ya que en un paso se obtiene un capicúa: 56+65=121.
57, ya que en dos pasos se obtiene un capicúa: 57+75=132, 132+231=363
59, ya que en dos pasos se obtiene un capicúa: 59+95=154, 154+451=605, 605+506=1111
89, ya que en 24 pasos se obtiene un capicúa.

En este ejercicio, pensado para la asignatura de Informática (del Grado de Matemáticas) vamos a buscar con Haskell el primer número de Lychrel.
Read More “Números de Lychrel”

Executable Multivariate Polynomials

PorJosé A. Alonso 11 agosto 20108 marzo 2013

Christian Sternagel y René Thiemann han publicado en The Archive of Formal Proofs el artículo Executable Multivariate Polynomials.

El artículo es parte del proyecto IsaFoR/CeTA (Isabelle Formalization of Rewriting / Certified Termination Analysis) cuyo objetivo es la formalización en Isabelle de técnicas de terminación. Los ficheros del proyecto se encuentran aquí.

Una de las técnicas usadas para demostrar la terminación de sistemas de reescritura se basa en las interpretaciones polinómicas.

En el artículo Executable Multivariate Polynomials se presenta una formalización en Isabelle de los polinomios con varias variables con coeficientes en un semianillo ordenado. Se definen las operaciones de polinomios (suma, multiplicación y sustitución) y la ordenación de polinomios. La formalización también incluye el criterio de Neurauter, Zankl y Middeldorp monotocidad de interpretaciones polinómicas sobre los naturales.

La función de Takeuchi como banco de prueba para la eficiencia

PorJosé A. Alonso 11 agosto 20109 abril 2014

La función de Takeuchi está definida por
$tak(x,y,z) = \newline \left\{ \begin{array}{ll} y, & si \ x \leq y \\ tak(tak(x-1,y,z), tak(y-1,z,x), tak(z-1,x,y)) & en\ caso\ contrario \end{array} \right.$

En este artículo voy a comparar la la eficiencia de Haskell, Maxima y Lisp escribiendo en los tres la definición recursiva de la función de Takeuchi y calculando $tak(16,6,1)$ .
Read More “La función de Takeuchi como banco de prueba para la eficiencia”

El número de Mersenne 47 en Haskell

PorJosé A. Alonso 9 agosto 20108 marzo 2013

En el artículo Cruce de listas abordamos el tema de la simplicidad y eficiencia de las soluciones. En este artículo deseo mostrar la capacidad de Haskell para calcular con grandes números enteros. Para ello, he elegido calcular el último primo de Mersenne descubierto.

Los números primos de Mersenne son los primos de la forma $2^n-1$ . El último primo de Mersenne descubierto es $M_{47}=2^{43112609}-1$ que es un número con más de 12 millones de cifras. El descubrimiento lo realizó Edson Smith el 23 de agosto de 2008. Dicho número es el 47 primo de Mersenne conocido.
Read More “El número de Mersenne 47 en Haskell”

Formal Power Series

PorJosé A. Alonso 8 agosto 20108 marzo 2013

Acaba de publicarse un nuevo artículo de razonamiento formalizado. El artículo es Formal Power Series publicado por Amine Chaieb en el Journal of Automated Reasoning.

El resumen que hace el autor del artículo es el siguiente: We present a formalization of the topological ring of formal power series in Isabelle/HOL. We also formalize formal derivatives, division, radicals, composition and reverses. As an application, we show how formal elementary and hyper-geometric series yield elegant proofs for some combinatorial identities. We easily derive a basic theory of polynomials. Then, using a generic formalization of the fraction field of an integral domain, we obtain formal Laurent series and rational functions for free.

La formalización completa se encuentra en Theory Formal Power Series