Reseña: Coinductive pearl: Modular first-order logic completeness

PorJosé A. Alonso

Se ha publicado un artículo de razonamiento formalizado en Isabelle/HOL sobre metalógica titulado Coinductive pearl: Modular first-order logic completeness.

Sus autores son Jasmin Christian Blanchette, Andrei Popescu y Dmitriy Traytel (de la Universidad Técnica de Munich).

Su resumen es

Codatatypes are unfortunately still missing in many programming languages and proof assistants. We make a case for their usefulness by revisiting a classic result: the completeness theorem for first-order logic established through a Gentzen system. Codatatypes help capture the essence of the proof, which establishes an abstract property of derivation trees independently of the concrete syntax or inference rules. This separation of concerns simplifies the presentation, especially for readers acquainted with lazy data structures. The proof is formalized in Isabelle/HOL and demonstrates the recently introduced definitional package for codatatypes and its integration with Isabelle’s Haskell code generator.

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

Reseña: Experience report: Teaching Haskell to the masses

PorJosé A. Alonso

Se ha publicado un artículo sobre la ensñanza de Haskell titulado Experience report: Teaching Haskell to the masses.

Sus autores son Jasmin Christian Blanchette, Tobias Nipkow, Lars Noschinski y Dmitriy Traytel (de la Universidad Técnica de Munich).

Su resumen es

We report on our experience teaching a Haskell-based functional programming course to over 600 students. The syllabus was organized around selected material from various sources. Throughout the term, we emphasized correctness through QuickCheck tests and proofs by induction. The submission architecture was coupled with automatic testing, giving students the possibility to correct mistakes before the deadline. To motivate the students, we complemented the weekly assignments with an informal competition.

I1M2012: Operaciones con el TAD de los polinomios en Haskell (1)

PorJosé A. Alonso

En la segunda parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se han resueltolos 5 primeros ejercicios de la relación 24. El objetivo de esta relación es ampliar el conjunto de operaciones
sobre polinomios definidas utilizando las implementaciones del TAD de
polinomio estudiadas en el tema 21. Además, en algunos ejemplos de usan polinomios con coeficientes racionales. En Haskell, el número racional x/y se representa por x%y. El TAD de los números racionales está definido en el módulo Data.Ratio.

En los ejercicios se usan las siguientes librerías, estudiadas en el tema 21,

  • PolRepTDA: Implementación de los polinomios mediante tipos de datos algebraicos.
  • PolRepDispersa: Implementación de los polinomios mediante listas dispersas.
  • PolRepDensa: Implementación de los polinomios mediante listas densas.
  • PolOperaciones: Operaciones con el TAD de los polinomios.

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: Operaciones con el TAD de los polinomios en Haskell (1)”

I1M2012: Combinatoria en Haskell (2)

PorJosé A. Alonso

En la primera parte de la clase de hoy de Informática de 1º del Grado en Matemáticas se ha completado las soluciones de los ejercicios de la relación 22 que se empezó en la clase de la semana pasada.

El objetivo de esta relación es estudiar la generación y el número de
las principales operaciones de la combinatoria. En concreto, se
estudia

  • Permutaciones.
  • Combinaciones sin repetición..
  • Combinaciones con repetición
  • Variaciones sin repetición.
  • Variaciones con repetición.

Además, se estudia dos temas relacionados:

  • Reconocimiento y generación de subconjuntos y
  • El triángulo de Pascal

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: Combinatoria en Haskell (2)”

I1M2012: Ejercicios de cálculo numérico en Haskell

PorJosé A. Alonso

En la clase de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios de la 22ª relación, en la que se definen funciones para resolver los siguientes problemas de cálculo numérico:

  • diferenciación numérica,
  • cálculo de la raíz cuadrada mediante el método de Herón,
  • cálculo de los ceros de una función por el método de Newton y
  • cálculo de funciones inversas.

Un aspecto a destacar desde el punto de vista de la programación es el uso de la abstracción de procedimientos.

Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: Ejercicios de cálculo numérico en Haskell”