I1M2014: Presentación del curso de Informática (de 1º de Matemáticas)

PorJosé A. Alonso

En la clase de hoy del curso de Informática (de 1º de Grado en Matemáticas) se ha presentado la asignatura siguiendo el resumen del proyecto docente y los materiales en la página de la asignatura:

Se ha explicado cómo instalar los sistemas y se ha mostrado una sesión sobre el uso de Haskell y emacs. La sesión está grabada en este vídeo.

Se ha comentado el sistema de evaluación y se ha anunciado las fechas de los exámenes de todo el curso.

Iteración, recursión y punto fijo

PorJosé A. Alonso

En esta relación de ejercicios se muestra cómo se pueden transformar programas iterativos (con bucles while o for) en programas en recursivos. Para cada uno de los bucles, se elige una función y se pide definirla usando el bucle (en Python), buscar una definición recursiva que sea semejante a la anterior, definir el patrón que abstrae el bucle, definirla con el patrón y aplicar el patrón a otras funciones. Finalmente, se estudia cómo definir algunas de las anteriores funciones usando el menor punto fijo.

Read More “Iteración, recursión y punto fijo”

Libro de exámenes de programación funcional con Haskell

PorJosé A. Alonso

He publicado una ampliación del libro Exámenes de programación funcional con Haskell (2009-2014). El libro es una recopilación de los exámenes de la asignatura de Informática (de primero del Grado en Matemáticas) desde el curso 2009-10 hasta el actual.

Tras la ampliación, el libro contiene 102 exámenes y 648 ejercicios.

Este libro es el complemento de los anteriores:

Reseña: Real-valued special functions: upper and lower bounds

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL titulado Real-valued special functions: upper and lower bounds

Su autor es Lawrence C. Paulson (de la Universidad de Cambridge).

Su resumen es

This development proves upper and lower bounds for several familiar real-valued functions. For sin, cos, exp and sqrt, it defines and verifies infinite families of upper and lower bounds, mostly based on Taylor series expansions. For arctan, ln and exp, it verifies a finite collection of upper and lower bounds, originally obtained from the functions’ continued fraction expansions using the computer algebra system Maple. A common theme in these proofs is to take the difference between a function and its approximation, which should be zero at one point, and then consider the sign of the derivative. The immediate purpose of this development is to verify axioms used by MetiTarski, an automatic theorem prover for real-valued special functions. Crucial to MetiTarski’s operation is the provision of upper and lower bounds for each function of interest.

El trabajo se ha publicado en en AFP (The Archive of Formal Proofs).

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