En la clase de hoy, se ha presentado el curso Lógica Informática siguiendo el plan de la asignatura. Se ha comentado el contenido de la asignatura, el sistema de evaluación y los materiales de la asignatura en la Red:
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.
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.
Hoy se ha realizado el 7º examen del curso de Informática (de 1º de Grado en Matemáticas). Este es el examen de la convocatoria de septiembre. Los ejercicios, y sus soluciones, se muestran a continuación.
Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre algorítmica titulado Amortized complexity verified.
Su autor es Tobias Nipkow (de la Technische Universität München).
Su resumen es
*A framework for the analysis of the amortized complexity of (functional) data structures is formalized in Isabelle/HOL and applied to two non-trivial examples: skew heaps and splay trees. In the same spirit we show that the move-to-front algorithm for the list update problem is 2-competitive. *
El trabajo se presentó en el Isabelle Workshop 2014.
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.