José A. Alonso

Introducción a la Demostración Asistida por Ordenador

PorJosé A. Alonso 7 agosto 20108 marzo 2013

Estoy escribiendo una Introducción a la Demostración Asistida por Ordenador (con Isabelle/Isar).

Su objetivo es servir de texto para la curso Demostración asistida por ordenador que empezará a impartirse el próximo curso 2010-11.

El libro parte de los apuntes usados en el Seminario del Grupo de Lógica Computacional del 2008.

Este libro es abierto. Iré anunciando las ampliaciones y actualizaciones en Vestigium.

Todos los comentarios serán bienvenidos e incorporados al libro.

Cruce de listas

PorJosé A. Alonso 5 agosto 20108 marzo 2013

En esta entrada comento las soluciones en Haskell y Maxima de un problema planteado por Adam Majewski en la lista de Maxima en forma de ejercicio para I1M y PD. Además, añadiré soluciones en otros lenguajes conforme las vaya recibiendo.

1. Solución en Haskell

En este ejercico se usarán las siguientes librerías

import Data.List
import Test.QuickCheck

1 2	import Data.List import Test.QuickCheck

Ejercicio 1. Definir la función

cruce :: Eq a => [a] -> [a] -> [[a]]

1	cruce :: Eq a => [a] -> [a] -> [[a]]

tal que (cruce xs ys) es la lista de las listas obtenidas con uniendo las listas de xs sin un elemento con las de ys sin un elemento. Por ejemplo,

*Main> cruce [1,5,3] [2,4]
[[5,3,4],[5,3,2],[1,3,4],[1,3,2],[1,5,4],[1,5,2]]
*Main> cruce [1,5,3] [2,4,6]
[[5,3,4,6],[5,3,2,6],[5,3,2,4],[1,3,4,6],[1,3,2,6],
 [1,3,2,4],[1,5,4,6],[1,5,2,6],[1,5,2,4]]

*Main> cruce [1,5,3] [2,4]

[[5,3,4],[5,3,2],[1,3,4],[1,3,2],[1,5,4],[1,5,2]]

*Main> cruce [1,5,3] [2,4,6]

[[5,3,4,6],[5,3,2,6],[5,3,2,4],[1,3,4,6],[1,3,2,6],

[1,3,2,4],[1,5,4,6],[1,5,2,6],[1,5,2,4]]

Cero elevado a cero y errores informáticos

PorJosé A. Alonso 4 agosto 20108 marzo 2013

Es muy frecuente los errores que se comenten al calcular el valor de “cero elevado a cero”. De esta forma, hay quienes piensan erróneamente que es un operación “prohibida”, que es una indeterminada o que su valor es 0.

En el artículo Cero elevado a la cero de Gustavo Piñeiro se explica detalladamente porqué cero elevado a cero es igual a uno.

Los errores sobre cero elevado a cero no sólo se dan entre los humanos, sino que también se dan en los sistemas informáticos. Maxima lo calcula erróneamente como se puede observar en la siguiente sesión
Read More “Cero elevado a cero y errores informáticos”

El problema de los números felices

PorJosé A. Alonso 3 agosto 20108 marzo 2013

1. El problema de los números felices

Según la Wikipedia, un número feliz se define por el siguiente proceso. Se comienza reemplazando el número por la suma del cuadrado de sus cifras y se repite el proceso hasta que se obtiene el número 1 o se entra en un ciclo que no contiene al 1. Aquellos números para los que el proceso termina en 1 se llaman números felices y los que entran en un ciclo sin 1 se llaman números desgraciados.

Por ejemplo, 7 es un número feliz porque

  7 ~> 7^2                              =  49
     ~> 4^2 + 9^2          = 16 + 81    =  97
     ~> 9^2 + 7^2          = 81 + 49    = 130
     ~> 1^2 + 3^2 + 0^2    =  1 + 9 + 0 =  10
     ~> 1^2 + 0^2          =  1 + 0     =   1

7 ~> 7^2 = 49

~> 4^2 + 9^2 = 16 + 81 = 97

~> 9^2 + 7^2 = 81 + 49 = 130

~> 1^2 + 3^2 + 0^2 = 1 + 9 + 0 = 10

~> 1^2 + 0^2 = 1 + 0 = 1

Pero 17 es un número desgraciado porque

   17 ~> 1^2 + 7^2           =  1 + 49        =  50
       ~> 5^2 + 0^2          = 25 +  0        =  25
       ~> 2^2 + 5^2          =  4 + 25        =  29
       ~> 2^2 + 9^2          =  4 + 81        =  85
       ~> 8^2 + 5^2          = 64 + 25        =  89
       ~> 8^2 + 9^2          = 64 + 81        = 145
       ~> 1^2 + 4^2 + 5^2    =  1 + 16 + 25   =  42
       ~> 4^2 + 2^2          = 16 +  4        =  20
       ~> 2^2 + 0^2          =  4 +  0        =   4
       ~> 4^2                                 =  16
       ~> 1^2 + 6^2          = 1 + 36         =  37
       ~> 3^2 + 7^2          = 9 + 49         =  58
       ~> 5^2 + 8^2          = 25 + 64        =  89

17 ~> 1^2 + 7^2 = 1 + 49 = 50

~> 5^2 + 0^2 = 25 + 0 = 25

~> 2^2 + 5^2 = 4 + 25 = 29

~> 2^2 + 9^2 = 4 + 81 = 85

~> 8^2 + 5^2 = 64 + 25 = 89

~> 8^2 + 9^2 = 64 + 81 = 145

~> 1^2 + 4^2 + 5^2 = 1 + 16 + 25 = 42

~> 4^2 + 2^2 = 16 + 4 = 20

~> 2^2 + 0^2 = 4 + 0 = 4

~> 4^2 = 16

~> 1^2 + 6^2 = 1 + 36 = 37

~> 3^2 + 7^2 = 9 + 49 = 58

~> 5^2 + 8^2 = 25 + 64 = 89

que forma un bucle al repetirse el 89.

El objetivo del ejercicio es definir una función que calcule todos los números felices hasta un límite dado.
Read More “El problema de los números felices”

Libro de introducción al cálculo simbólico con Maxima

PorJosé A. Alonso 1 agosto 20108 marzo 2013

He aprovechado los primeros días no laborables para recopilar el material sobre cálculo simbólico en Maxima que he usado en las asignaturas Informática de 1º de Matemáticas) y Sofware libre para la enseñanza y aprendizaje de las Matemáticas. Fruto de dicha recopilación es el libro Introducción a Maxima.

En el libro se hace una presentación de Maxima a través de ejercicios resueltos (que se comentan en clases) y propuestos (para resolver por los alumnos en la wiki de la asignatura y, posteriormente, comentar as soluciones en clase).

Esta es la primera versión del libro y he incluido también las soluciones de los ejercicios propuestos. Espero vuestros comentarios para las siguientes versiones.