Vestigium

Errores aritméticos en Haskell y en Lisp

PorJosé A. Alonso 8 enero 20118 marzo 2013

La primera vez que uno se encuentra con los siguientes cálculos aritméticos en Haskell puede sorprenderse.

~> ghci
GHCi, version 6.12.1: http://www.haskell.org/ghc/  
ghci> 1.1 == 1.1
True
ghci> 1.1+1.1 == 2.2
True
ghci> 1.1+1.1+1.1 == 3.3
False
ghci> 2.2+1.1 == 3.3
False

~> ghci

GHCi, version 6.12.1: http://www.haskell.org/ghc/

ghci> 1.1 == 1.1

True

ghci> 1.1+1.1 == 2.2

True

ghci> 1.1+1.1+1.1 == 3.3

False

ghci> 2.2+1.1 == 3.3

False

El mismo comportamiento se da en Common Lisp

~> clisp
Welcome to GNU CLISP 2.44.1 (2008-02-23) <http://clisp.cons.org/>

[1]> (= 1.1 1.1)
T
[2]> (= (+ 1.1 1.1) 2.2)
T
[3]> (= (+ 1.1 1.1 1.1) 3.3)
NIL
[4]> (= (+ 1.1 2.2) 3.3)
NIL

~> clisp

Welcome to GNU CLISP 2.44.1 (2008-02-23) <http://clisp.cons.org/>

[1]> (= 1.1 1.1)

[2]> (= (+ 1.1 1.1) 2.2)

[3]> (= (+ 1.1 1.1 1.1) 3.3)

NIL

[4]> (= (+ 1.1 2.2) 3.3)

NIL

Para comprender estos cálculos es aconsejable leer What Every Computer Scientist Should Know About Floating-Point Arithmetic.

El 2011 y los números primos (en Haskell)

PorJosé A. Alonso 6 enero 20118 marzo 2013

Cada comienzo de año se suelen buscar propiedades numéricas del número del año. En el 2011 se han buscado propiedades que relacionan el 2011 y los números primos.

En este ejercicio (para la asignatura Informática (de 1º del Grado en Matemáticas)) vamos a realizar la búsqueda de dichas propiedades con Haskell.
Read More “El 2011 y los números primos (en Haskell)”

Teorías y aplicaciones

PorJosé A. Alonso 29 diciembre 20108 marzo 2013

Existe una contraposición entre el desarrollo teórico y el aplicado. Aunque a veces se prefiere el aplicado, conviene recordar la siguiente cita de Karl Weierstrass

A la pregunta de si es realmente posible sacar algún provecho de las teorías abstractas que la matemática moderna parece apoyar, uno debería contestar que fue basándose únicamente en la especulación pura como los matemáticos griegos dedujeron las propiedades de las cónicas, mucho antes de que nadie pudiera imaginarse que representan las órbitas de los planetas.

Reseña: Certifying compilers using higher-order theorem provers as certificate checkers

PorJosé A. Alonso 23 diciembre 20108 marzo 2013

Jan Olaf Blech y Benjamin Grégoire han publicado el artículo Certifying compilers using higher-order theorem provers as certificate checkers en la revista Formal Methods in System Design.

El resumen del artículo es
Read More “Reseña: Certifying compilers using higher-order theorem provers as certificate checkers”

RA2010: Razonamiento por inducción sobre los naturales

PorJosé A. Alonso 21 diciembre 20108 marzo 2013

La clase de hoy del curso de Razonamiento automático ha tenido dos partes. En la primera parte se ha comentado la historia del razonamiento automático y algunos de sus logros. En la segunda parte se ha continuado la introducción de técnicas de demostración en Isabelle estudiando la demostración por inducción sobre los números naturales.

Las transparencias y apuntes usados en clase son los siguientes:

La tarea pendiente para la próxima clase consiste en escribir, y publicar en el portafolio digital, las soluciones de los ejercicios de la relación 1 y de la relación 2. Los códigos se encuentran el la página de ejercicios.